Theorem axcclem 9279

Description: Lemma for axcc 9280. (Contributed by Mario Carneiro, 2-Feb-2013.) (Revised by Mario Carneiro, 16-Nov-2013.)

Hypotheses

Ref	Expression
axcclem.1	|- A = ( x \ { (/) } )
axcclem.2	|- F = ( n e. om , y e. U. A |-> ( f ` n ) )
axcclem.3	|- G = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )

Assertion

Ref	Expression
axcclem	|- ( x ~~ om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )

Distinct variable groups:   A, f, h, n, y   w, A, z, f, h   h, F, z   g, G, z   f, g, x, h

Allowed substitution hints:   A( x, g)   F( x, y, w, f, g, n)   G( x, y, w, f, h, n)

Proof of Theorem axcclem

Dummy variables c i k are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfinite2 8218	. . . . . . . 8 |- ( A ~< om -> A e. Fin )
2		axcclem.1	. . . . . . . . . 10 |- A = ( x \ { (/) } )
3	2	eleq1i 2692	. . . . . . . . 9 |- ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
4		undif1 4043	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
5		snfi 8038	. . . . . . . . . . . 12 |- { (/) } e. Fin
6		unfi 8227	. . . . . . . . . . . 12 |- ( ( ( x \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
7	5, 6	mpan2 707	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) e. Fin -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
8	4, 7	syl5eqelr 2706	. . . . . . . . . 10 |- ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
9		ssun1 3776	. . . . . . . . . 10 |- x C_ ( x u. { (/) } )
10		ssfi 8180	. . . . . . . . . 10 |- ( ( ( x u. { (/) } ) e. Fin /\ x C_ ( x u. { (/) } ) ) -> x e. Fin )
11	8, 9, 10	sylancl 694	. . . . . . . . 9 |- ( ( x \ { (/) } ) e. Fin -> x e. Fin )
12	3, 11	sylbi 207	. . . . . . . 8 |- ( A e. Fin -> x e. Fin )
13		dcomex 9269	. . . . . . . . . 10 |- om e. _V
14		isfiniteg 8220	. . . . . . . . . 10 |- ( om e. _V -> ( x e. Fin <-> x ~< om ) )
15	13, 14	ax-mp 5	. . . . . . . . 9 |- ( x e. Fin <-> x ~< om )
16		sdomnen 7984	. . . . . . . . 9 |- ( x ~< om -> -. x ~~ om )
17	15, 16	sylbi 207	. . . . . . . 8 |- ( x e. Fin -> -. x ~~ om )
18	1, 12, 17	3syl 18	. . . . . . 7 |- ( A ~< om -> -. x ~~ om )
19	18	con2i 134	. . . . . 6 |- ( x ~~ om -> -. A ~< om )
20		sdomentr 8094	. . . . . . 7 |- ( ( A ~< x /\ x ~~ om ) -> A ~< om )
21	20	expcom 451	. . . . . 6 |- ( x ~~ om -> ( A ~< x -> A ~< om ) )
22	19, 21	mtod 189	. . . . 5 |- ( x ~~ om -> -. A ~< x )
23		vex 3203	. . . . . 6 |- x e. _V
24		difss 3737	. . . . . . 7 |- ( x \ { (/) } ) C_ x
25	2, 24	eqsstri 3635	. . . . . 6 |- A C_ x
26		ssdomg 8001	. . . . . 6 |- ( x e. _V -> ( A C_ x -> A ~<_ x ) )
27	23, 25, 26	mp2 9	. . . . 5 |- A ~<_ x
28	22, 27	jctil 560	. . . 4 |- ( x ~~ om -> ( A ~<_ x /\ -. A ~< x ) )
29		bren2 7986	. . . 4 |- ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
30	28, 29	sylibr 224	. . 3 |- ( x ~~ om -> A ~~ x )
31		entr 8008	. . 3 |- ( ( A ~~ x /\ x ~~ om ) -> A ~~ om )
32	30, 31	mpancom 703	. 2 |- ( x ~~ om -> A ~~ om )
33		ensym 8005	. 2 |- ( A ~~ om -> om ~~ A )
34		bren 7964	. . 3 |- ( om ~~ A <-> E. f f : om -1-1-onto-> A )
35		f1of 6137	. . . . . . . 8 |- ( f : om -1-1-onto-> A -> f : om --> A )
36		peano1 7085	. . . . . . . 8 |- (/) e. om
37		ffvelrn 6357	. . . . . . . 8 |- ( ( f : om --> A /\ (/) e. om ) -> ( f ` (/) ) e. A )
38	35, 36, 37	sylancl 694	. . . . . . 7 |- ( f : om -1-1-onto-> A -> ( f ` (/) ) e. A )
39		eldifn 3733	. . . . . . . . 9 |- ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
40	39, 2	eleq2s 2719	. . . . . . . 8 |- ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
41		fvex 6201	. . . . . . . . . . 11 |- ( f ` (/) ) e. _V
42	41	elsn 4192	. . . . . . . . . 10 |- ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
43	42	notbii 310	. . . . . . . . 9 |- ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
44		neq0 3930	. . . . . . . . 9 |- ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
45	43, 44	bitr2i 265	. . . . . . . 8 |- ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
46	40, 45	sylibr 224	. . . . . . 7 |- ( ( f ` (/) ) e. A -> E. c c e. ( f ` (/) ) )
47	38, 46	syl 17	. . . . . 6 |- ( f : om -1-1-onto-> A -> E. c c e. ( f ` (/) ) )
48		elunii 4441	. . . . . . . . . . 11 |- ( ( c e. ( f ` (/) ) /\ ( f ` (/) ) e. A ) -> c e. U. A )
49	38, 48	sylan2 491	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> c e. U. A )
50	35	ffvelrnda 6359	. . . . . . . . . . . . . 14 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> ( f ` n ) e. A )
51		difabs 3892	. . . . . . . . . . . . . . . . . 18 |- ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
52	2	difeq1i 3724	. . . . . . . . . . . . . . . . . 18 |- ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
53	51, 52, 2	3eqtr4i 2654	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) = A
54		pwuni 4474	. . . . . . . . . . . . . . . . . 18 |- A C_ ~P U. A
55		ssdif 3745	. . . . . . . . . . . . . . . . . 18 |- ( A C_ ~P U. A -> ( A \ { (/) } ) C_ ( ~P U. A \ { (/) } ) )
56	54, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) C_ ( ~P U. A \ { (/) } )
57	53, 56	eqsstr3i 3636	. . . . . . . . . . . . . . . 16 |- A C_ ( ~P U. A \ { (/) } )
58	57	sseli 3599	. . . . . . . . . . . . . . 15 |- ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
59	58	ralrimivw 2967	. . . . . . . . . . . . . 14 |- ( ( f ` n ) e. A -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
60	50, 59	syl 17	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
61	60	ralrimiva 2966	. . . . . . . . . . . 12 |- ( f : om -1-1-onto-> A -> A. n e. om A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
62		axcclem.2	. . . . . . . . . . . . 13 |- F = ( n e. om , y e. U. A |-> ( f ` n ) )
63	62	fmpt2 7237	. . . . . . . . . . . 12 |- ( A. n e. om A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) <-> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
64	61, 63	sylib 208	. . . . . . . . . . 11 |- ( f : om -1-1-onto-> A -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
65	64	adantl 482	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
66		difexg 4808	. . . . . . . . . . . . . 14 |- ( x e. _V -> ( x \ { (/) } ) e. _V )
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 |- ( x \ { (/) } ) e. _V
68	2, 67	eqeltri 2697	. . . . . . . . . . . 12 |- A e. _V
69	68	uniex 6953	. . . . . . . . . . 11 |- U. A e. _V
70	69	axdc4 9278	. . . . . . . . . 10 |- ( ( c e. U. A /\ F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) ) -> E. h ( h : om --> U. A /\ ( h ` (/) ) = c /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
71	49, 65, 70	syl2anc 693	. . . . . . . . 9 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> E. h ( h : om --> U. A /\ ( h ` (/) ) = c /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
72		3simpb 1059	. . . . . . . . . 10 |- ( ( h : om --> U. A /\ ( h ` (/) ) = c /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
73	72	eximi 1762	. . . . . . . . 9 |- ( E. h ( h : om --> U. A /\ ( h ` (/) ) = c /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> E. h ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
74	71, 73	syl 17	. . . . . . . 8 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> E. h ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
75	74	ex 450	. . . . . . 7 |- ( c e. ( f ` (/) ) -> ( f : om -1-1-onto-> A -> E. h ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) )
76	75	exlimiv 1858	. . . . . 6 |- ( E. c c e. ( f ` (/) ) -> ( f : om -1-1-onto-> A -> E. h ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) )
77	47, 76	mpcom 38	. . . . 5 |- ( f : om -1-1-onto-> A -> E. h ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) )
78		velsn 4193	. . . . . . . . . . 11 |- ( z e. { (/) } <-> z = (/) )
79	78	necon3bbii 2841	. . . . . . . . . 10 |- ( -. z e. { (/) } <-> z =/= (/) )
80	2	eleq2i 2693	. . . . . . . . . . 11 |- ( z e. A <-> z e. ( x \ { (/) } ) )
81		eldif 3584	. . . . . . . . . . 11 |- ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82	80, 81	sylbbr 226	. . . . . . . . . 10 |- ( ( z e. x /\ -. z e. { (/) } ) -> z e. A )
83	79, 82	sylan2br 493	. . . . . . . . 9 |- ( ( z e. x /\ z =/= (/) ) -> z e. A )
84		simpl 473	. . . . . . . . . . . 12 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> f : om -1-1-onto-> A )
85		f1ofo 6144	. . . . . . . . . . . . . 14 |- ( f : om -1-1-onto-> A -> f : om -onto-> A )
86		foelrn 6378	. . . . . . . . . . . . . 14 |- ( ( f : om -onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
87	85, 86	sylan 488	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
88		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> suc k = suc i )
89	88	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
90		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> k = i )
91		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> ( h ` k ) = ( h ` i ) )
92	90, 91	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
93	89, 92	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
94	93	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. om -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95	94	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
96	95	imp 445	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) )
97	96	3adant3 1081	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc i ) e. ( i F ( h ` i ) ) )
98		eqcom 2629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = ( f ` i ) <-> ( f ` i ) = z )
99		f1ocnvfv 6534	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
100	98, 99	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
101	100	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102	101	imp 445	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> ( `' f ` z ) = i )
103	102	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
104	103	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105		suceq 5790	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = ( `' f ` z ) -> suc i = suc ( `' f ` z ) )
106	104, 105	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> suc i = suc ( `' f ` z ) )
107	106	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc i ) = ( h ` suc ( `' f ` z ) ) )
108		simpr 477	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> i e. om )
109		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> ( h ` i ) e. U. A )
110		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = i -> ( f ` n ) = ( f ` i ) )
111		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
112		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f ` i ) e. _V
113	110, 111, 62, 112	ovmpt2 6796	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. om /\ ( h ` i ) e. U. A ) -> ( i F ( h ` i ) ) = ( f ` i ) )
114	108, 109, 113	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
115	114	3adant2 1080	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
116	115	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117	97, 107, 116	3eltr3d 2715	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( h ` suc ( `' f ` z ) ) e. ( f ` i ) )
118	35	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
119	118	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
120	119	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( f ` i ) e. A )
121		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
122	121	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( z e. A <-> ( f ` i ) e. A ) )
123	120, 122	mpbird 247	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> z e. A )
124		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
125		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( `' f ` w ) = ( `' f ` z ) -> suc ( `' f ` w ) = suc ( `' f ` z ) )
126	124, 125	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w = z -> suc ( `' f ` w ) = suc ( `' f ` z ) )
127	126	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = z -> ( h ` suc ( `' f ` w ) ) = ( h ` suc ( `' f ` z ) ) )
128		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 |- G = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
129		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21 |- ( h ` suc ( `' f ` z ) ) e. _V
130	127, 128, 129	fvmpt 6282	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. A -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
131	123, 130	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
132		simp3 1063	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> z = ( f ` i ) )
133	117, 131, 132	3eltr4d 2716	. . . . . . . . . . . . . . . . . 18 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) /\ z = ( f ` i ) ) -> ( G ` z ) e. z )
134	133	3exp 1264	. . . . . . . . . . . . . . . . 17 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( z = ( f ` i ) -> ( G ` z ) e. z ) ) )
135	134	com3r 87	. . . . . . . . . . . . . . . 16 |- ( z = ( f ` i ) -> ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) )
136	135	3expd 1284	. . . . . . . . . . . . . . 15 |- ( z = ( f ` i ) -> ( h : om --> U. A -> ( f : om -1-1-onto-> A -> ( i e. om -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) ) )
137	136	com4r 94	. . . . . . . . . . . . . 14 |- ( i e. om -> ( z = ( f ` i ) -> ( h : om --> U. A -> ( f : om -1-1-onto-> A -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) ) )
138	137	rexlimiv 3027	. . . . . . . . . . . . 13 |- ( E. i e. om z = ( f ` i ) -> ( h : om --> U. A -> ( f : om -1-1-onto-> A -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) )
139	87, 138	syl 17	. . . . . . . . . . . 12 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> ( h : om --> U. A -> ( f : om -1-1-onto-> A -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) ) )
140	84, 139	mpid 44	. . . . . . . . . . 11 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> ( h : om --> U. A -> ( A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) -> ( G ` z ) e. z ) ) )
141	140	impd 447	. . . . . . . . . 10 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> ( ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) -> ( G ` z ) e. z ) )
142	141	impancom 456	. . . . . . . . 9 |- ( ( f : om -1-1-onto-> A /\ ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( z e. A -> ( G ` z ) e. z ) )
143	83, 142	syl5 34	. . . . . . . 8 |- ( ( f : om -1-1-onto-> A /\ ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( ( z e. x /\ z =/= (/) ) -> ( G ` z ) e. z ) )
144	143	expd 452	. . . . . . 7 |- ( ( f : om -1-1-onto-> A /\ ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> ( z e. x -> ( z =/= (/) -> ( G ` z ) e. z ) ) )
145	144	ralrimiv 2965	. . . . . 6 |- ( ( f : om -1-1-onto-> A /\ ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) )
146		fvrn0 6216	. . . . . . . . . . 11 |- ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
147	146	rgenw 2924	. . . . . . . . . 10 |- A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
148		eqid 2622	. . . . . . . . . . 11 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
149	148	fmpt 6381	. . . . . . . . . 10 |- ( A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } ) <-> ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } ) )
150	147, 149	mpbi 220	. . . . . . . . 9 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
151		vex 3203	. . . . . . . . . . 11 |- h e. _V
152	151	rnex 7100	. . . . . . . . . 10 |- ran h e. _V
153		p0ex 4853	. . . . . . . . . 10 |- { (/) } e. _V
154	152, 153	unex 6956	. . . . . . . . 9 |- ( ran h u. { (/) } ) e. _V
155		fex2 7121	. . . . . . . . 9 |- ( ( ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } ) /\ A e. _V /\ ( ran h u. { (/) } ) e. _V ) -> ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V )
156	150, 68, 154, 155	mp3an 1424	. . . . . . . 8 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
157	128, 156	eqeltri 2697	. . . . . . 7 |- G e. _V
158		fveq1 6190	. . . . . . . . . 10 |- ( g = G -> ( g ` z ) = ( G ` z ) )
159	158	eleq1d 2686	. . . . . . . . 9 |- ( g = G -> ( ( g ` z ) e. z <-> ( G ` z ) e. z ) )
160	159	imbi2d 330	. . . . . . . 8 |- ( g = G -> ( ( z =/= (/) -> ( g ` z ) e. z ) <-> ( z =/= (/) -> ( G ` z ) e. z ) ) )
161	160	ralbidv 2986	. . . . . . 7 |- ( g = G -> ( A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) ) )
162	157, 161	spcev 3300	. . . . . 6 |- ( A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
163	145, 162	syl 17	. . . . 5 |- ( ( f : om -1-1-onto-> A /\ ( h : om --> U. A /\ A. k e. om ( h ` suc k ) e. ( k F ( h ` k ) ) ) ) -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
164	77, 163	exlimddv 1863	. . . 4 |- ( f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
165	164	exlimiv 1858	. . 3 |- ( E. f f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166	34, 165	sylbi 207	. 2 |- ( om ~~ A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
167	32, 33, 166	3syl 18	1 |- ( x ~~ om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   `'ccnv 5113   ran crn 5115   suc csuc 5725   -->wf 5884   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   omcom 7065   ~~ cen 7952   ~<_ cdom 7953   ~< csdm 7954   Fincfn 7955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-dc 9268

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959

This theorem is referenced by:  axcc  9280