Theorem tz7.49 3954

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 groups:   x,y,F   x,A,y

Proof of Theorem tz7.49

Step	Hyp	Ref	Expression
1		tz7.49.2	. . . . . . 7 |- A e. V
2		tz7.48.1	. . . . . . . 8 |- F Fn On
3	2	tz7.48-3 3953	. . . . . . 7 |- (A.x e. On (F` x) e. (A \ (F"x)) -> -. A e. V)
4	1, 3	mt2 109	. . . . . 6 |- -. A.x e. On (F` x) e. (A \ (F"x))
5		r19.20 1700	. . . . . . 7 |- (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		df-ne 1585	. . . . . . . 8 |- ((A \ (F"x)) =/= (/) <-> -. (A \ (F"x)) = (/))
7	6	ralbii 1665	. . . . . . 7 |- (A.x e. On (A \ (F"x)) =/= (/) <-> A.x e. On -. (A \ (F"x)) = (/))
8	5, 7	syl5ibr 207	. . . . . 6 |- (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))))
9	4, 8	mtoi 107	. . . . 5 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> -. A.x e. On -. (A \ (F"x)) = (/))
10		dfrex2 1654	. . . . 5 |- (E.x e. On (A \ (F"x)) = (/) <-> -. A.x e. On -. (A \ (F"x)) = (/))
11	9, 10	sylibr 200	. . . 4 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> E.x e. On (A \ (F"x)) = (/))
12		imaeq2 3398	. . . . . . 7 |- (x = y -> (F"x) = (F"y))
13	12	difeq2d 2156	. . . . . 6 |- (x = y -> (A \ (F"x)) = (A \ (F"y)))
14	13	eqeq1d 1481	. . . . 5 |- (x = y -> ((A \ (F"x)) = (/) <-> (A \ (F"y)) = (/)))
15	14	onminex 3016	. . . 4 |- (E.x e. On (A \ (F"x)) = (/) -> E.x e. On ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
16	11, 15	syl 10	. . 3 |- (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)) = (/)))
17		df-ne 1585	. . . . . 6 |- ((A \ (F"y)) =/= (/) <-> -. (A \ (F"y)) = (/))
18	17	ralbii 1665	. . . . 5 |- (A.y e. x (A \ (F"y)) =/= (/) <-> A.y e. x -. (A \ (F"y)) = (/))
19	18	anbi2i 480	. . . 4 |- (((A \ (F"x)) = (/) /\ A.y e. x (A \ (F"y)) =/= (/)) <-> ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
20	19	rexbii 1666	. . 3 |- (E.x e. On ((A \ (F"x)) = (/) /\ A.y e. x (A \ (F"y)) =/= (/)) <-> E.x e. On ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
21	16, 20	sylibr 200	. 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)) =/= (/)))
22		hbra1 1685	. . 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))))
23		pm3.27 323	. . . . . . . . 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)) =/= (/))
24	23	ad2antrr 404	. . . . . . . 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)) =/= (/))
25		ax-17 970	. . . . . . . . . . . . . . . 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))))
26		hbra1 1685	. . . . . . . . . . . . . . . 16 |- (A.y e. x (A \ (F"y)) =/= (/) -> A.yA.y e. x (A \ (F"y)) =/= (/))
27	25, 26	hban 1008	. . . . . . . . . . . . . . 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)) =/= (/)))
28		ax-17 970	. . . . . . . . . . . . . . 15 |- ((x e. On -> z e. A) -> A.y(x e. On -> z e. A))
29		ra4 1692	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y e. x (A \ (F"y)) =/= (/) -> (y e. x -> (A \ (F"y)) =/= (/)))
30	29	adantld 390	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.y e. x (A \ (F"y)) =/= (/) -> ((x e. On /\ y e. x) -> (A \ (F"y)) =/= (/)))
31		onelon 2968	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. On /\ y e. x) -> y e. On)
32	13	neeq1d 1592	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> ((A \ (F"x)) =/= (/) <-> (A \ (F"y)) =/= (/)))
33		fveq2 3719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = y -> (F` x) = (F` y))
34	33, 13	eleq12d 1540	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> ((F` x) e. (A \ (F"x)) <-> (F` y) e. (A \ (F"y))))
35	32, 34	imbi12d 625	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = y -> (((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) <-> ((A \ (F"y)) =/= (/) -> (F` y) e. (A \ (F"y)))))
36	35	rcla4v 1870	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. On -> (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> ((A \ (F"y)) =/= (/) -> (F` y) e. (A \ (F"y)))))
37	36	com23 32	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. On -> ((A \ (F"y)) =/= (/) -> (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (F` y) e. (A \ (F"y)))))
38	31, 37	syl 10	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. On /\ y e. x) -> ((A \ (F"y)) =/= (/) -> (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (F` y) e. (A \ (F"y)))))
39	30, 38	sylcom 51	. . . . . . . . . . . . . . . . . . . . 21 |- (A.y e. x (A \ (F"y)) =/= (/) -> ((x e. On /\ y e. x) -> (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (F` y) e. (A \ (F"y)))))
40	39	com3r 35	. . . . . . . . . . . . . . . . . . . 20 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (A.y e. x (A \ (F"y)) =/= (/) -> ((x e. On /\ y e. x) -> (F` y) e. (A \ (F"y)))))
41	40