Theorem tz7.49 5168

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 5167	. . . . . . 7 |- (A.x e. On (F` x) e. (A \ (F"x)) -> -. A e. _V)
4	1, 3	mt2 124	. . . . . 6 |- -. A.x e. On (F` x) e. (A \ (F"x))
5		ralim 2164	. . . . . . 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 2019	. . . . . . . 8 |- ((A \ (F"x)) =/= (/) <-> -. (A \ (F"x)) = (/))
7	6	ralbii 2127	. . . . . . 7 |- (A.x e. On (A \ (F"x)) =/= (/) <-> A.x e. On -. (A \ (F"x)) = (/))
8	5, 7	syl5ibr 224	. . . . . 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 122	. . . . 5 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> -. A.x e. On -. (A \ (F"x)) = (/))
10		dfrex2 2116	. . . . 5 |- (E.x e. On (A \ (F"x)) = (/) <-> -. A.x e. On -. (A \ (F"x)) = (/))
11	9, 10	sylibr 217	. . . 4 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> E.x e. On (A \ (F"x)) = (/))
12		imaeq2 4260	. . . . . . 7 |- (x = y -> (F"x) = (F"y))
13	12	difeq2d 2726	. . . . . 6 |- (x = y -> (A \ (F"x)) = (A \ (F"y)))
14	13	eqeq1d 1892	. . . . 5 |- (x = y -> ((A \ (F"x)) = (/) <-> (A \ (F"y)) = (/)))
15	14	onminex 3888	. . . 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 12	. . 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 2019	. . . . . 6 |- ((A \ (F"y)) =/= (/) <-> -. (A \ (F"y)) = (/))
18	17	ralbii 2127	. . . . 5 |- (A.y e. x (A \ (F"y)) =/= (/) <-> A.y e. x -. (A \ (F"y)) = (/))
19	18	anbi2i 538	. . . 4 |- (((A \ (F"x)) = (/) /\ A.y e. x (A \ (F"y)) =/= (/)) <-> ((A \ (F"x)) = (/) /\ A.y e. x -. (A \ (F"y)) = (/)))
20	19	rexbii 2128	. . 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 217	. 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 2147	. . 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		simpllr 453	. . . . . . . 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)) =/= (/))
24		ax-17 1317	. . . . . . . . . . . . . . . 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))))
25		hbra1 2147	. . . . . . . . . . . . . . . 16 |- (A.y e. x (A \ (F"y)) =/= (/) -> A.yA.y e. x (A \ (F"y)) =/= (/))
26	24, 25	hban 1356	. . . . . . . . . . . . . . 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)) =/= (/)))
27		ax-17 1317	. . . . . . . . . . . . . . 15 |- ((x e. On -> z e. A) -> A.y(x e. On -> z e. A))
28		ra4 2155	. . . . . . . . . . . . . . . . . . . . . . 23 |- (A.y e. x (A \ (F"y)) =/= (/) -> (y e. x -> (A \ (F"y)) =/= (/)))
29	28	adantld 426	. . . . . . . . . . . . . . . . . . . . . 22 |- (A.y e. x (A \ (F"y)) =/= (/) -> ((x e. On /\ y e. x) -> (A \ (F"y)) =/= (/)))
30		onelon 3683	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((x e. On /\ y e. x) -> y e. On)
31	13	neeq1d 2028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> ((A \ (F"x)) =/= (/) <-> (A \ (F"y)) =/= (/)))
32		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = y -> (F` x) = (F` y))
33	32, 13	eleq12d 1965	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = y -> ((F` x) e. (A \ (F"x)) <-> (F` y) e. (A \ (F"y))))
34	31, 33	imbi12d 688	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = y -> (((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) <-> ((A \ (F"y)) =/= (/) -> (F` y) e. (A \ (F"y)))))
35	34	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . . . 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)))))
36	35	com23 36	. . . . . . . . . . . . . . . . . . . . . . 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)))))
37	30, 36	syl 12	. . . . . . . . . . . . . . . . . . . . . 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)))))
38	29, 37	sylcom 62	. . . . . . . . . . . . . . . . . . . . 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)))))
39	38	com3r 39	. . . . . . . . . . . . . . . . . . . 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)))))
40	39	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((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	exp3a 405	. . . . . . . . . . . . . . . . . 18 |- ((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)))))
42	41	com23 36	. . . . . . . . . . . . . . . . 17 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (y e. x -> (x e. On -> (F` y) e. (A \ (F"y)))))
43		eleq1 1957	. . . . . . . . . . . . . . . . . 18 |- ((F` y) = z -> ((F` y) e. A <-> z e. A))
44		eldifi 2730	. . . . . . . . . . . . . . . . . 18 |- ((F` y) e. (A \ (F"y)) -> (F` y) e. A)
45	43, 44	syl5cbi 226	. . . . . . . . . . . . . . . . 17 |- ((F` y) e. (A \ (F"y)) -> ((F` y) = z -> z e. A))
46	42, 45	syl8 27	. . . . . . . . . . . . . . . 16 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (y e. x -> (x e. On -> ((F` y) = z -> z e. A))))
47	46	com34 40	. . . . . . . . . . . . . . 15 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (y e. x -> ((F` y) = z -> (x e. On -> z e. A))))
48	26, 27, 47	r19.23ad 2213	. . . . . . . . . . . . . 14 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (E.y e. x (F` y) = z -> (x e. On -> z e. A)))
49		fnfun 4510	. . . . . . . . . . . . . . . 16 |- (F Fn On -> Fun F)
50	2, 49	ax-mp 7	. . . . . . . . . . . . . . 15 |- Fun F
51		fvelima 4723	. . . . . . . . . . . . . . 15 |- ((Fun F /\ z e. (F"x)) -> E.y e. x (F` y) = z)
52	50, 51	mpan 759	. . . . . . . . . . . . . 14 |- (z e. (F"x) -> E.y e. x (F` y) = z)
53	48, 52	syl5 20	. . . . . . . . . . . . 13 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (z e. (F"x) -> (x e. On -> z e. A)))
54	53	com23 36	. . . . . . . . . . . 12 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (x e. On -> (z e. (F"x) -> z e. A)))
55	54	imp 377	. . . . . . . . . . 11 |- (((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) /\ x e. On) -> (z e. (F"x) -> z e. A))
56	55	ssrdv 2622	. . . . . . . . . 10 |- (((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) /\ x e. On) -> (F"x) C_ A)
57		ssdif0 2934	. . . . . . . . . . 11 |- (A C_ (F"x) <-> (A \ (F"x)) = (/))
58	57	biimpri 169	. . . . . . . . . 10 |- ((A \ (F"x)) = (/) -> A C_ (F"x))
59	56, 58	anim12i 360	. . . . . . . . 9 |- ((((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)) = (/)) -> ((F"x) C_ A /\ A C_ (F"x)))
60		eqss 2631	. . . . . . . . 9 |- ((F"x) = A <-> ((F"x) C_ A /\ A C_ (F"x)))
61	59, 60	sylibr 217	. . . . . . . 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)) = (/)) -> (F"x) = A)
62	25, 24	hban 1356	. . . . . . . . . . . . . . . 16 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> A.y(A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))))
63		ax-17 1317	. . . . . . . . . . . . . . . 16 |- (x C_ On -> A.y x C_ On)
64		ssel 2615	. . . . . . . . . . . . . . . . . . . . 21 |- (x C_ On -> (y e. x -> y e. On))
65		funfvima2 4829	. . . . . . . . . . . . . . . . . . . . . 22 |- ((Fun F /\ y C_ dom F) -> (z e. y -> (F` z) e. (F"y)))
66		onss 3869	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y e. On -> y C_ On)
67		fndm 4512	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F Fn On -> dom F = On)
68	2, 67	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . 23 |- dom F = On
69	66, 68	syl6ssr 2664	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. On -> y C_ dom F)
70	65, 50, 69	sylancr 526	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. On -> (z e. y -> (F` z) e. (F"y)))
71	64, 70	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- (x C_ On -> (y e. x -> (z e. y -> (F` z) e. (F"y))))
72	28	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. x -> (A.y e. x (A \ (F"y)) =/= (/) -> (A \ (F"y)) =/= (/)))
73	72	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x C_ On -> (y e. x -> (A.y e. x (A \ (F"y)) =/= (/) -> (A \ (F"y)) =/= (/))))
74	64, 36	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x C_ 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))))))
75	73, 74	syldd 61	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x C_ On -> (y e. x -> (A.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))))))
76	75	imp4a 391	. . . . . . . . . . . . . . . . . . . . . 22 |- (x C_ On -> (y e. x -> ((A.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)))))
77		eleq1a 1966	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F` z) e. (F"y) -> ((F` y) = (F` z) -> (F` y) e. (F"y)))
78	77	con3d 111	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` z) e. (F"y) -> (-. (F` y) e. (F"y) -> -. (F` y) = (F` z)))
79		eldifn 2731	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F` y) e. (A \ (F"y)) -> -. (F` y) e. (F"y))
80	78, 79	syl5com 63	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F` y) e. (A \ (F"y)) -> ((F` z) e. (F"y) -> -. (F` y) = (F` z)))
81	76, 80	syl8 27	. . . . . . . . . . . . . . . . . . . . 21 |- (x C_ On -> (y e. x -> ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> ((F` z) e. (F"y) -> -. (F` y) = (F` z)))))
82	81	com34 40	. . . . . . . . . . . . . . . . . . . 20 |- (x C_ On -> (y e. x -> ((F` z) e. (F"y) -> ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> -. (F` y) = (F` z)))))
83	71, 82	syldd 61	. . . . . . . . . . . . . . . . . . 19 |- (x C_ On -> (y e. x -> (z e. y -> ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> -. (F` y) = (F` z)))))
84	83	com4r 45	. . . . . . . . . . . . . . . . . 18 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> (y e. x -> (z e. y -> -. (F` y) = (F` z)))))
85	84	imp4a 391	. . . . . . . . . . . . . . . . 17 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> ((y e. x /\ z e. y) -> -. (F` y) = (F` z))))
86	85	19.21adv 1666	. . . . . . . . . . . . . . . 16 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> A.z((y e. x /\ z e. y) -> -. (F` y) = (F` z))))
87	62, 63, 86	19.21ad 1406	. . . . . . . . . . . . . . 15 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> A.yA.z((y e. x /\ z e. y) -> -. (F` y) = (F` z))))
88		r2al 2136	. . . . . . . . . . . . . . 15 |- (A.y e. x A.z e. y -. (F` y) = (F` z) <-> A.yA.z((y e. x /\ z e. y) -> -. (F` y) = (F` z)))
89	87, 88	syl6ibr 230	. . . . . . . . . . . . . 14 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> A.y e. x A.z e. y -. (F` y) = (F` z)))
90	89	ancld 322	. . . . . . . . . . . . 13 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> (x C_ On /\ A.y e. x A.z e. y -. (F` y) = (F` z))))
91	2	tz7.48lem 5164	. . . . . . . . . . . . 13 |- ((x C_ On /\ A.y e. x A.z e. y -. (F` y) = (F` z)) -> Fun `'(F |` x))
92	90, 91	syl6 25	. . . . . . . . . . . 12 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x C_ On -> Fun `'(F |` x)))
93		onss 3869	. . . . . . . . . . . 12 |- (x e. On -> x C_ On)
94	92, 93	syl5 20	. . . . . . . . . . 11 |- ((A.y e. x (A \ (F"y)) =/= (/) /\ A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x)))) -> (x e. On -> Fun `'(F |` x)))
95	94	ancoms 484	. . . . . . . . . 10 |- ((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (x e. On -> Fun `'(F |` x)))
96	95	imp 377	. . . . . . . . 9 |- (((A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) /\ A.y e. x (A \ (F"y)) =/= (/)) /\ x e. On) -> Fun `'(F |` x))
97	96	adantr 425	. . . . . . . 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)) = (/)) -> Fun `'(F |` x))
98	23, 61, 97	3jca 1050	. . . . . . 7 |- ((((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)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x)))
99	98	exp41 413	. . . . . 6 |- (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)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x))))))
100	99	com23 36	. . . . 5 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (x e. On -> (A.y e. x (A \ (F"y)) =/= (/) -> ((A \ (F"x)) = (/) -> (A.y e. x (A \ (F"y)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x))))))
101	100	com34 40	. . . 4 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (x e. On -> ((A \ (F"x)) = (/) -> (A.y e. x (A \ (F"y)) =/= (/) -> (A.y e. x (A \ (F"y)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x))))))
102	101	imp4a 391	. . 3 |- (A.x e. On ((A \ (F"x)) =/= (/) -> (F` x) e. (A \ (F"x))) -> (x e. On -> (((A \ (F"x)) = (/) /\ A.y e. x (A \ (F"y)) =/= (/)) -> (A.y e. x (A \ (F"y)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x)))))
103	22, 102	reximdai 2199	. 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)) =/= (/)) -> E.x e. On (A.y e. x (A \ (F"y)) =/= (/) /\ (F"x) = A /\ Fun `'(F |` x))))
104	21, 103	mpd 29	1 |- (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)))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   C_ wss 2593  (/)c0 2875  Oncon0 3657  `'ccnv 3985  dom cdm 3986   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  ` cfv 3998

This theorem is referenced by:  tz7.49c 5169

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fv 4014

Copyright terms: Public domain