Theorem axcclem 8871

Description: Lemma for axcc 8872. (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 7814	. . . . . . . 8 |- ( A ~< om -> A e. Fin )
2		axcclem.1	. . . . . . . . . 10 |- A = ( x \ { (/) } )
3	2	eleq1i 2481	. . . . . . . . 9 |- ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
4		undif1 3849	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
5		snfi 7636	. . . . . . . . . . . 12 |- { (/) } e. Fin
6		unfi 7823	. . . . . . . . . . . 12 |- ( ( ( x \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
7	5, 6	mpan2 671	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) e. Fin -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
8	4, 7	syl5eqelr 2497	. . . . . . . . . 10 |- ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
9		ssun1 3608	. . . . . . . . . 10 |- x C_ ( x u. { (/) } )
10		ssfi 7777	. . . . . . . . . 10 |- ( ( ( x u. { (/) } ) e. Fin /\ x C_ ( x u. { (/) } ) ) -> x e. Fin )
11	8, 9, 10	sylancl 662	. . . . . . . . 9 |- ( ( x \ { (/) } ) e. Fin -> x e. Fin )
12	3, 11	sylbi 197	. . . . . . . 8 |- ( A e. Fin -> x e. Fin )
13		dcomex 8861	. . . . . . . . . 10 |- om e. _V
14		isfiniteg 7816	. . . . . . . . . 10 |- ( om e. _V -> ( x e. Fin <-> x ~< om ) )
15	13, 14	ax-mp 5	. . . . . . . . 9 |- ( x e. Fin <-> x ~< om )
16		sdomnen 7584	. . . . . . . . 9 |- ( x ~< om -> -. x ~~ om )
17	15, 16	sylbi 197	. . . . . . . 8 |- ( x e. Fin -> -. x ~~ om )
18	1, 12, 17	3syl 18	. . . . . . 7 |- ( A ~< om -> -. x ~~ om )
19	18	con2i 122	. . . . . 6 |- ( x ~~ om -> -. A ~< om )
20		sdomentr 7691	. . . . . . 7 |- ( ( A ~< x /\ x ~~ om ) -> A ~< om )
21	20	expcom 435	. . . . . 6 |- ( x ~~ om -> ( A ~< x -> A ~< om ) )
22	19, 21	mtod 179	. . . . 5 |- ( x ~~ om -> -. A ~< x )
23		vex 3064	. . . . . 6 |- x e. _V
24		difss 3572	. . . . . . 7 |- ( x \ { (/) } ) C_ x
25	2, 24	eqsstri 3474	. . . . . 6 |- A C_ x
26		ssdomg 7601	. . . . . 6 |- ( x e. _V -> ( A C_ x -> A ~<_ x ) )
27	23, 25, 26	mp2 9	. . . . 5 |- A ~<_ x
28	22, 27	jctil 537	. . . 4 |- ( x ~~ om -> ( A ~<_ x /\ -. A ~< x ) )
29		bren2 7586	. . . 4 |- ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
30	28, 29	sylibr 214	. . 3 |- ( x ~~ om -> A ~~ x )
31		entr 7607	. . 3 |- ( ( A ~~ x /\ x ~~ om ) -> A ~~ om )
32	30, 31	mpancom 669	. 2 |- ( x ~~ om -> A ~~ om )
33		ensym 7604	. 2 |- ( A ~~ om -> om ~~ A )
34		bren 7565	. . 3 |- ( om ~~ A <-> E. f f : om -1-1-onto-> A )
35		f1of 5801	. . . . . . . 8 |- ( f : om -1-1-onto-> A -> f : om --> A )
36		peano1 6705	. . . . . . . 8 |- (/) e. om
37		ffvelrn 6009	. . . . . . . 8 |- ( ( f : om --> A /\ (/) e. om ) -> ( f ` (/) ) e. A )
38	35, 36, 37	sylancl 662	. . . . . . 7 |- ( f : om -1-1-onto-> A -> ( f ` (/) ) e. A )
39		eldifn 3568	. . . . . . . . 9 |- ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
40	39, 2	eleq2s 2512	. . . . . . . 8 |- ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
41		fvex 5861	. . . . . . . . . . 11 |- ( f ` (/) ) e. _V
42	41	elsnc 3998	. . . . . . . . . 10 |- ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
43	42	notbii 296	. . . . . . . . 9 |- ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
44		neq0 3751	. . . . . . . . 9 |- ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
45	43, 44	bitr2i 252	. . . . . . . 8 |- ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
46	40, 45	sylibr 214	. . . . . . 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 4198	. . . . . . . . . . 11 |- ( ( c e. ( f ` (/) ) /\ ( f ` (/) ) e. A ) -> c e. U. A )
49	38, 48	sylan2 474	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> c e. U. A )
50	35	ffvelrnda 6011	. . . . . . . . . . . . . 14 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> ( f ` n ) e. A )
51		difabs 3716	. . . . . . . . . . . . . . . . . 18 |- ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
52	2	difeq1i 3559	. . . . . . . . . . . . . . . . . 18 |- ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
53	51, 52, 2	3eqtr4i 2443	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) = A
54		pwuni 4624	. . . . . . . . . . . . . . . . . 18 |- A C_ ~P U. A
55		ssdif 3580	. . . . . . . . . . . . . . . . . 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 3475	. . . . . . . . . . . . . . . 16 |- A C_ ( ~P U. A \ { (/) } )
58	57	sseli 3440	. . . . . . . . . . . . . . 15 |- ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
59	58	ralrimivw 2821	. . . . . . . . . . . . . 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 2820	. . . . . . . . . . . 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 6853	. . . . . . . . . . . 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 198	. . . . . . . . . . 11 |- ( f : om -1-1-onto-> A -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
65	64	adantl 466	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
66		difexg 4544	. . . . . . . . . . . . . 14 |- ( x e. _V -> ( x \ { (/) } ) e. _V )
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 |- ( x \ { (/) } ) e. _V
68	2, 67	eqeltri 2488	. . . . . . . . . . . 12 |- A e. _V
69	68	uniex 6580	. . . . . . . . . . 11 |- U. A e. _V
70	69	axdc4 8870	. . . . . . . . . 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 661	. . . . . . . . 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 997	. . . . . . . . . 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 1679	. . . . . . . . 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 434	. . . . . . 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 1745	. . . . . 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 36	. . . . 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		elsn 3988	. . . . . . . . . . 11 |- ( z e. { (/) } <-> z = (/) )
79	78	necon3bbii 2666	. . . . . . . . . 10 |- ( -. z e. { (/) } <-> z =/= (/) )
80	2	eleq2i 2482	. . . . . . . . . . . 12 |- ( z e. A <-> z e. ( x \ { (/) } ) )
81		eldif 3426	. . . . . . . . . . . 12 |- ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82	80, 81	bitri 251	. . . . . . . . . . 11 |- ( z e. A <-> ( z e. x /\ -. z e. { (/) } ) )
83	82	biimpri 208	. . . . . . . . . 10 |- ( ( z e. x /\ -. z e. { (/) } ) -> z e. A )
84	79, 83	sylan2br 476	. . . . . . . . 9 |- ( ( z e. x /\ z =/= (/) ) -> z e. A )
85		simpl 457	. . . . . . . . . . . 12 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> f : om -1-1-onto-> A )
86		f1ofo 5808	. . . . . . . . . . . . . 14 |- ( f : om -1-1-onto-> A -> f : om -onto-> A )
87		foelrn 6030	. . . . . . . . . . . . . 14 |- ( ( f : om -onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
88	86, 87	sylan 471	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
89		suceq 5477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> suc k = suc i )
90	89	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
91		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> k = i )
92		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> ( h ` k ) = ( h ` i ) )
93	91, 92	oveq12d 6298	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
94	90, 93	eleq12d 2486	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95	94	rspcv 3158	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( 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	3ad2ant3 1022	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
97	96	imp 429	. . . . . . . . . . . . . . . . . . . . 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 ) ) )
98	97	3adant3 1019	. . . . . . . . . . . . . . . . . . . 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 ) ) )
99		eqcom 2413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = ( f ` i ) <-> ( f ` i ) = z )
100		f1ocnvfv 6167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
101	99, 100	syl5bi 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102	101	3adant1 1017	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
103	102	imp 429	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> ( `' f ` z ) = i )
104	103	eqcomd 2412	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105	104	3adant2 1018	. . . . . . . . . . . . . . . . . . . . . 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 ) )
106		suceq 5477	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = ( `' f ` z ) -> suc i = suc ( `' f ` z ) )
107	105, 106	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 ) )
108	107	fveq2d 5855	. . . . . . . . . . . . . . . . . . . 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 ) ) )
109		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> i e. om )
110		ffvelrn 6009	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> ( h ` i ) e. U. A )
111		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = i -> ( f ` n ) = ( f ` i ) )
112		eqidd 2405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
113		fvex 5861	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f ` i ) e. _V
114	111, 112, 62, 113	ovmpt2 6421	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. om /\ ( h ` i ) e. U. A ) -> ( i F ( h ` i ) ) = ( f ` i ) )
115	109, 110, 114	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
116	115	3adant2 1018	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117	116	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . . 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 ) )
118	98, 108, 117	3eltr3d 2506	. . . . . . . . . . . . . . . . . . 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 ) )
119	35	ffvelrnda 6011	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
120	119	3adant1 1017	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
121	120	3ad2ant1 1020	. . . . . . . . . . . . . . . . . . . . 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 )
122		eleq1 2476	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
123	122	3ad2ant3 1022	. . . . . . . . . . . . . . . . . . . . 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 ) )
124	121, 123	mpbird 234	. . . . . . . . . . . . . . . . . . . 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 )
125		fveq2 5851	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
126		suceq 5477	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( `' f ` w ) = ( `' f ` z ) -> suc ( `' f ` w ) = suc ( `' f ` z ) )
127	125, 126	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w = z -> suc ( `' f ` w ) = suc ( `' f ` z ) )
128	127	fveq2d 5855	. . . . . . . . . . . . . . . . . . . . 21 |- ( w = z -> ( h ` suc ( `' f ` w ) ) = ( h ` suc ( `' f ` z ) ) )
129		axcclem.3	. . . . . . . . . . . . . . . . . . . . 21 |- G = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
130		fvex 5861	. . . . . . . . . . . . . . . . . . . . 21 |- ( h ` suc ( `' f ` z ) ) e. _V
131	128, 129, 130	fvmpt 5934	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. A -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
132	124, 131	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 ) ) )
133		simp3 1001	. . . . . . . . . . . . . . . . . . 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 ) )
134	118, 132, 133	3eltr4d 2507	. . . . . . . . . . . . . . . . . 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 )
135	134	3exp 1198	. . . . . . . . . . . . . . . . 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 ) ) )
136	135	com3r 81	. . . . . . . . . . . . . . . 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 ) ) )
137	136	3expd 1216	. . . . . . . . . . . . . . 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 ) ) ) ) )
138	137	com4r 88	. . . . . . . . . . . . . 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 ) ) ) ) )
139	138	rexlimiv 2892	. . . . . . . . . . . . 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 ) ) ) )
140	88, 139	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 ) ) ) )
141	85, 140	mpid 41	. . . . . . . . . . 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 ) ) )
142	141	impd 431	. . . . . . . . . 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 ) )
143	142	impancom 440	. . . . . . . . 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 ) )
144	84, 143	syl5 32	. . . . . . . 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 ) )
145	144	expd 436	. . . . . . 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 ) ) )
146	145	ralrimiv 2818	. . . . . 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 ) )
147		fvrn0 5873	. . . . . . . . . . 11 |- ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
148	147	rgenw 2767	. . . . . . . . . 10 |- A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
149		eqid 2404	. . . . . . . . . . 11 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
150	149	fmpt 6032	. . . . . . . . . 10 |- ( A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } ) <-> ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } ) )
151	148, 150	mpbi 210	. . . . . . . . 9 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
152		vex 3064	. . . . . . . . . . 11 |- h e. _V
153	152	rnex 6720	. . . . . . . . . 10 |- ran h e. _V
154		p0ex 4583	. . . . . . . . . 10 |- { (/) } e. _V
155	153, 154	unex 6582	. . . . . . . . 9 |- ( ran h u. { (/) } ) e. _V
156		fex2 6741	. . . . . . . . 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 )
157	151, 68, 155, 156	mp3an 1328	. . . . . . . 8 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
158	129, 157	eqeltri 2488	. . . . . . 7 |- G e. _V
159		fveq1 5850	. . . . . . . . . 10 |- ( g = G -> ( g ` z ) = ( G ` z ) )
160	159	eleq1d 2473	. . . . . . . . 9 |- ( g = G -> ( ( g ` z ) e. z <-> ( G ` z ) e. z ) )
161	160	imbi2d 316	. . . . . . . 8 |- ( g = G -> ( ( z =/= (/) -> ( g ` z ) e. z ) <-> ( z =/= (/) -> ( G ` z ) e. z ) ) )
162	161	ralbidv 2845	. . . . . . 7 |- ( g = G -> ( A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) <-> A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) ) )
163	158, 162	spcev 3153	. . . . . 6 |- ( A. z e. x ( z =/= (/) -> ( G ` z ) e. z ) -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
164	146, 163	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 ) )
165	77, 164	exlimddv 1749	. . . 4 |- ( f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166	165	exlimiv 1745	. . 3 |- ( E. f f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
167	34, 166	sylbi 197	. 2 |- ( om ~~ A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
168	32, 33, 167	3syl 18	1 |- ( x ~~ om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 186   /\ wa 369   /\ w3a 976   = wceq 1407   E.wex 1635   e. wcel 1844   =/= wne 2600   A.wral 2756   E.wrex 2757   _Vcvv 3061   \ cdif 3413   u. cun 3414   C_ wss 3416   (/)c0 3740   ~Pcpw 3957   {csn 3974   U.cuni 4193   class class class wbr 4397   |-> cmpt 4455   X. cxp 4823   `'ccnv 4824   ran crn 4826   suc csuc 5414   -->wf 5567   -onto->wfo 5569   -1-1-onto->wf1o 5570   ` cfv 5571  (class class class)co 6280   |-> cmpt2 6282   omcom 6685   ~~ cen 7553   ~<_ cdom 7554   ~< csdm 7555   Fincfn 7556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-8 1846  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pow 4574  ax-pr 4632  ax-un 6576  ax-dc 8860

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3or 977  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3063  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3741  df-if 3888  df-pw 3959  df-sn 3975  df-pr 3977  df-tp 3979  df-op 3981  df-uni 4194  df-int 4230  df-iun 4275  df-br 4398  df-opab 4456  df-mpt 4457  df-tr 4492  df-eprel 4736  df-id 4740  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-xp 4831  df-rel 4832  df-cnv 4833  df-co 4834  df-dm 4835  df-rn 4836  df-res 4837  df-ima 4838  df-pred 5369  df-ord 5415  df-on 5416  df-lim 5417  df-suc 5418  df-iota 5535  df-fun 5573  df-fn 5574  df-f 5575  df-f1 5576  df-fo 5577  df-f1o 5578  df-fv 5579  df-ov 6283  df-oprab 6284  df-mpt2 6285  df-om 6686  df-1st 6786  df-2nd 6787  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-1o 7169  df-oadd 7173  df-er 7350  df-en 7557  df-dom 7558  df-sdom 7559  df-fin 7560

This theorem is referenced by:  axcc  8872