Theorem tz7.49 2997

Description: Proposition 7.49 of [TakeutiZaring] p. 51.

Hypotheses

Ref	Expression
tz7.48.1	|- F Fn On
tz7.49.2	|- A e. V

Assertion

Ref	Expression
tz7.49	|- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> E.x e. On (A.y e. x -. (A \ (F"y)) = (/) /\ (F"x) = A /\ Fun `'(F |` x)))

Distinct variable group(s):   x,y,F   x,A,y

Proof of Theorem tz7.49

Step	Hyp	Ref	Expression
1		tz7.49.2	. . . . . 6 |- A e. V
2		tz7.48.1	. . . . . . 7 |- F Fn On
3	2	tz7.48-3 2996	. . . . . 6 |- (A.x e. On (F` x) e. (A \ (F"x)) -> -. A e. V)
4	1, 3	mt2 96	. . . . 5 |- -. A.x e. On (F` x) e. (A \ (F"x))
5		r19.20 1251	. . . . 5 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> (A.x e. On -. (A \ (F"x)) = (/) -> A.x e. On (F` x) e. (A \ (F"x))))
6	4, 5	mtoi 94	. . . 4 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> -. A.x e. On -. (A \ (F"x)) = (/))
7		dfrex2 1212	. . . 4 |- (E.x e. On (A \ (F"x)) = (/) <-> -. A.x e. On -. (A \ (F"x)) = (/))
8	6, 7	sylibr 175	. . 3 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> E.x e. On (A \ (F"x)) = (/))
9		imaeq2 2603	. . . . . 6 |- (x = y -> (F"x) = (F"y))
10	9	difeq2d 1588	. . . . 5 |- (x = y -> (A \ (F"x)) = (A \ (F"y)))
11	10	cleq1d 1109	. . . 4 |- (x = y -> ((A \ (F"x)) = (/) <-> (A \ (F"y)) = (/)))
12	11	onminex 2275	. . 3 |- (E.x e. On (A \ (F"x)) = (/) -> E.x e. On ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
13	8, 12	syl 12	. 2 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> E.x e. On ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
14		hbra1 1237	. . 3 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> A.xA.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))))
15		pm3.27 260	. . . . . . . . 9 |- ((A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x -. (A \ (F"y)) = (/)) -> A.y e. x -. (A \ (F"y)) = (/))
16	15	ad2antll 320	. . . . . . . 8 |- ((((A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x -. (A \ (F"y)) = (/)) /\ x e. On) /\ (A \ (F"x)) = (/)) -> A.y e. x -. (A \ (F"y)) = (/))
17		ax-17 925	. . . . . . . . . . . . . . . 16 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> A.yA.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))))
18		hbra1 1237	. . . . . . . . . . . . . . . 16 |- (A.y e. x -. (A \ (F"y)) = (/) -> A.yA.y e. x -. (A \ (F"y)) = (/))
19	17, 18	hban 704	. . . . . . . . . . . . . . 15 |- ((A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x -. (A \ (F"y)) = (/)) -> A.y(A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x -. (A \ (F"y)) = (/)))
20		ax-17 925	. . . . . . . . . . . . . . 15 |- ((x e. On -> z e. A) -> A.y(x e. On -> z e. A))
21	11	negbid 463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> (-. (A \ (F"x)) = (/) <-> -. (A \ (F"y)) = (/)))
22		fveq2 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = y -> (F` x) = (F` y))
23	22, 10	eleq12d 1157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> ((F` x) e. (A \ (F"x)) <-> (F` y) e. (A \ (F"y))))
24	21, 23	imbi12d 474	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = y -> ((-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) <-> (-. (A \ (F"y)) = (/) -> (F` y) e. (A \ (F"y)))))
25	24	rcla4v 1402	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> (y e. On -> (-. (A \ (F"y)) = (/) -> (F` y) e. (A \ (F"y)))))
26		eleq1 1149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F` y) = z -> ((F` y) e. A <-> z e. A))
27		eldifi 1591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F` y) e. (A \ (F"y)) -> (F` y) e. A)
28	26, 27	syl5bi 183	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F` y) = z -> ((F` y) e. (A \ (F"y)) -> z e. A))
29	28	com12 13	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` y) e. (A \ (F"y)) -> ((F` y) = z -> z e. A))
30	25, 29	syl8 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> (y e. On -> (-. (A \ (F"y)) = (/) -> ((F` y) = z -> z e. A))))
31		onelon 2223	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((x e. On /\ y e. x) -> y e. On)
32	31	ancoms 334	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((y e. x /\ x e. On) -> y e. On)
33	30, 32	syl5 22	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> ((y e. x /\ x e. On) -> (-. (A \ (F"y)) = (/) -> ((F` y) = z -> z e. A))))
34		ra4 1243	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y e. x -. (A \ (F"y)) = (/) -> (y e. x -> -. (A \ (F"y)) = (/)))
35	34	imp 277	. . . . . . . . . . . . . . . . . . . . . 22 |- ((A.y e. x -. (A \ (F"y)) = (/) /\ y e. x) -> -. (A \ (F"y)) = (/))
36	33, 35	syl7 24	. . . . . . . . . . . . . . . . . . . . 21 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> ((y e. x /\ x e. On) -> ((A.y e. x -. (A \ (F"y)) = (/) /\ y e. x) -> ((F` y) = z -> z e. A))))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . 20 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> ((A.y e. x -. (A \ (F"y)) = (/) /\ y e. x) -> ((y e. x /\ x e. On) -> ((F` y) = z -> z e. A))))
38	37	exp4a 295	. . . . . . . . . . . . . . . . . . 19 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> ((A.y e. x -. (A \ (F"y)) = (/) /\ y e. x) -> (y e. x -> (x e. On -> ((F` y) = z -> z e. A)))))
39	38	exp3a 292	. . . . . . . . . . . . . . . . . 18 |- (A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) -> (A.y e. x -. (A \ (F"y)) = (/) -> (y e. x -> (y e. x -> (x e. On -> ((F` y) = z -> z e. A))))))
40	39	imp 277	. . . . . . . . . . . . . . . . 17 |- ((A.x e. On (-. (A \ (F"x)) = (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x -. (A \ (F"y)) = (/)) -> (y e. x -> (y e. x -> (x e. On -> ((F` y) = z -> z e. A)))))
41	40	pm2.43d 59	. . . . . . . . . . . . . . . 16 |- ((A.x e. On (-. (A \ (F"