Theorem axcclem 8833

Description: Lemma for axcc 8834. (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 7774	. . . . . . . 8 |- ( A ~< om -> A e. Fin )
2		axcclem.1	. . . . . . . . . 10 |- A = ( x \ { (/) } )
3	2	eleq1i 2544	. . . . . . . . 9 |- ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
4		undif1 3902	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
5		snfi 7593	. . . . . . . . . . . 12 |- { (/) } e. Fin
6		unfi 7783	. . . . . . . . . . . 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 2560	. . . . . . . . . 10 |- ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
9		ssun1 3667	. . . . . . . . . 10 |- x C_ ( x u. { (/) } )
10		ssfi 7737	. . . . . . . . . 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 195	. . . . . . . 8 |- ( A e. Fin -> x e. Fin )
13		dcomex 8823	. . . . . . . . . 10 |- om e. _V
14		isfiniteg 7776	. . . . . . . . . 10 |- ( om e. _V -> ( x e. Fin <-> x ~< om ) )
15	13, 14	ax-mp 5	. . . . . . . . 9 |- ( x e. Fin <-> x ~< om )
16		sdomnen 7541	. . . . . . . . 9 |- ( x ~< om -> -. x ~~ om )
17	15, 16	sylbi 195	. . . . . . . 8 |- ( x e. Fin -> -. x ~~ om )
18	1, 12, 17	3syl 20	. . . . . . 7 |- ( A ~< om -> -. x ~~ om )
19	18	con2i 120	. . . . . 6 |- ( x ~~ om -> -. A ~< om )
20		sdomentr 7648	. . . . . . 7 |- ( ( A ~< x /\ x ~~ om ) -> A ~< om )
21	20	expcom 435	. . . . . 6 |- ( x ~~ om -> ( A ~< x -> A ~< om ) )
22	19, 21	mtod 177	. . . . 5 |- ( x ~~ om -> -. A ~< x )
23		vex 3116	. . . . . 6 |- x e. _V
24		difss 3631	. . . . . . 7 |- ( x \ { (/) } ) C_ x
25	2, 24	eqsstri 3534	. . . . . 6 |- A C_ x
26		ssdomg 7558	. . . . . 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 7543	. . . 4 |- ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
30	28, 29	sylibr 212	. . 3 |- ( x ~~ om -> A ~~ x )
31		entr 7564	. . 3 |- ( ( A ~~ x /\ x ~~ om ) -> A ~~ om )
32	30, 31	mpancom 669	. 2 |- ( x ~~ om -> A ~~ om )
33		ensym 7561	. 2 |- ( A ~~ om -> om ~~ A )
34		bren 7522	. . 3 |- ( om ~~ A <-> E. f f : om -1-1-onto-> A )
35		f1of 5814	. . . . . . . 8 |- ( f : om -1-1-onto-> A -> f : om --> A )
36		peano1 6697	. . . . . . . 8 |- (/) e. om
37		ffvelrn 6017	. . . . . . . 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 3627	. . . . . . . . 9 |- ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
40	39, 2	eleq2s 2575	. . . . . . . 8 |- ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
41		fvex 5874	. . . . . . . . . . 11 |- ( f ` (/) ) e. _V
42	41	elsnc 4051	. . . . . . . . . 10 |- ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
43	42	notbii 296	. . . . . . . . 9 |- ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
44		neq0 3795	. . . . . . . . 9 |- ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
45	43, 44	bitr2i 250	. . . . . . . 8 |- ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
46	40, 45	sylibr 212	. . . . . . 7 |- ( ( f ` (/) ) e. A -> E. c c e. ( f ` (/) ) )
47	38, 46	syl 16	. . . . . 6 |- ( f : om -1-1-onto-> A -> E. c c e. ( f ` (/) ) )
48		elunii 4250	. . . . . . . . . . 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 6019	. . . . . . . . . . . . . 14 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> ( f ` n ) e. A )
51		difabs 3762	. . . . . . . . . . . . . . . . . 18 |- ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
52	2	difeq1i 3618	. . . . . . . . . . . . . . . . . 18 |- ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
53	51, 52, 2	3eqtr4i 2506	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) = A
54		pwuni 4678	. . . . . . . . . . . . . . . . . 18 |- A C_ ~P U. A
55		ssdif 3639	. . . . . . . . . . . . . . . . . 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 3535	. . . . . . . . . . . . . . . 16 |- A C_ ( ~P U. A \ { (/) } )
58	57	sseli 3500	. . . . . . . . . . . . . . 15 |- ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
59	58	ralrimivw 2879	. . . . . . . . . . . . . 14 |- ( ( f ` n ) e. A -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
60	50, 59	syl 16	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> A. y e. U. A ( f ` n ) e. ( ~P U. A \ { (/) } ) )
61	60	ralrimiva 2878	. . . . . . . . . . . 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 6848	. . . . . . . . . . . 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 196	. . . . . . . . . . 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 4595	. . . . . . . . . . . . . 14 |- ( x e. _V -> ( x \ { (/) } ) e. _V )
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 |- ( x \ { (/) } ) e. _V
68	2, 67	eqeltri 2551	. . . . . . . . . . . 12 |- A e. _V
69	68	uniex 6578	. . . . . . . . . . 11 |- U. A e. _V
70	69	axdc4 8832	. . . . . . . . . 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 994	. . . . . . . . . 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 1635	. . . . . . . . 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 16	. . . . . . . 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 1698	. . . . . 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 4041	. . . . . . . . . . 11 |- ( z e. { (/) } <-> z = (/) )
79	78	necon3bbii 2728	. . . . . . . . . 10 |- ( -. z e. { (/) } <-> z =/= (/) )
80	2	eleq2i 2545	. . . . . . . . . . . 12 |- ( z e. A <-> z e. ( x \ { (/) } ) )
81		eldif 3486	. . . . . . . . . . . 12 |- ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82	80, 81	bitri 249	. . . . . . . . . . 11 |- ( z e. A <-> ( z e. x /\ -. z e. { (/) } ) )
83	82	biimpri 206	. . . . . . . . . 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 5821	. . . . . . . . . . . . . 14 |- ( f : om -1-1-onto-> A -> f : om -onto-> A )
87		foelrn 6038	. . . . . . . . . . . . . 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 4943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> suc k = suc i )
90	89	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
91		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> k = i )
92		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> ( h ` k ) = ( h ` i ) )
93	91, 92	oveq12d 6300	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
94	90, 93	eleq12d 2549	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95	94	rspcv 3210	. . . . . . . . . . . . . . . . . . . . . . 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 1019	. . . . . . . . . . . . . . . . . . . . . 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 1016	. . . . . . . . . . . . . . . . . . . 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 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = ( f ` i ) <-> ( f ` i ) = z )
100		f1ocnvfv 6170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
101	99, 100	syl5bi 217	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102	101	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105	104	3adant2 1015	. . . . . . . . . . . . . . . . . . . . . 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 4943	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = ( `' f ` z ) -> suc i = suc ( `' f ` z ) )
107	105, 106	syl 16	. . . . . . . . . . . . . . . . . . . . 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 5868	. . . . . . . . . . . . . . . . . . . 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 6017	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> ( h ` i ) e. U. A )
111		fveq2 5864	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = i -> ( f ` n ) = ( f ` i ) )
112		eqidd 2468	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
113		fvex 5874	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f ` i ) e. _V
114	111, 112, 62, 113	ovmpt2 6420	. . . . . . . . . . . . . . . . . . . . . . 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 1015	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117	116	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . 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 2569	. . . . . . . . . . . . . . . . . . 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 6019	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
120	119	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
121	120	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . . . 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 2539	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
123	122	3ad2ant3 1019	. . . . . . . . . . . . . . . . . . . . 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 232	. . . . . . . . . . . . . . . . . . . 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 5864	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
126		suceq 4943	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( `' f ` w ) = ( `' f ` z ) -> suc ( `' f ` w ) = suc ( `' f ` z ) )
127	125, 126	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( w = z -> suc ( `' f ` w ) = suc ( `' f ` z ) )
128	127	fveq2d 5868	. . . . . . . . . . . . . . . . . . . . 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 5874	. . . . . . . . . . . . . . . . . . . . 21 |- ( h ` suc ( `' f ` z ) ) e. _V
131	128, 129, 130	fvmpt 5948	. . . . . . . . . . . . . . . . . . . 20 |- ( z e. A -> ( G ` z ) = ( h ` suc ( `' f ` z ) ) )
132	124, 131	syl 16	. . . . . . . . . . . . . . . . . . 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 998	. . . . . . . . . . . . . . . . . . 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 2570	. . . . . . . . . . . . . . . . . 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 1195	. . . . . . . . . . . . . . . . 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 79	. . . . . . . . . . . . . . . 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 1213	. . . . . . . . . . . . . . 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 86	. . . . . . . . . . . . . 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 2949	. . . . . . . . . . . . 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 16	. . . . . . . . . . . 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 2876	. . . . . 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 5886	. . . . . . . . . . 11 |- ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
148	147	rgenw 2825	. . . . . . . . . 10 |- A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
149		eqid 2467	. . . . . . . . . . 11 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
150	149	fmpt 6040	. . . . . . . . . 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 208	. . . . . . . . 9 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
152		vex 3116	. . . . . . . . . . 11 |- h e. _V
153	152	rnex 6715	. . . . . . . . . 10 |- ran h e. _V
154		p0ex 4634	. . . . . . . . . 10 |- { (/) } e. _V
155	153, 154	unex 6580	. . . . . . . . 9 |- ( ran h u. { (/) } ) e. _V
156		fex2 6736	. . . . . . . . 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 1324	. . . . . . . 8 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
158	129, 157	eqeltri 2551	. . . . . . 7 |- G e. _V
159		fveq1 5863	. . . . . . . . . 10 |- ( g = G -> ( g ` z ) = ( G ` z ) )
160	159	eleq1d 2536	. . . . . . . . 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 2903	. . . . . . 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 3205	. . . . . 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 16	. . . . 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 1702	. . . 4 |- ( f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166	165	exlimiv 1698	. . 3 |- ( E. f f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
167	34, 166	sylbi 195	. 2 |- ( om ~~ A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
168	32, 33, 167	3syl 20	1 |- ( x ~~ om -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   \ cdif 3473   u. cun 3474   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   {csn 4027   U.cuni 4245   class class class wbr 4447   |-> cmpt 4505   suc csuc 4880   X. cxp 4997   `'ccnv 4998   ran crn 5000   -->wf 5582   -onto->wfo 5584   -1-1-onto->wf1o 5585   ` cfv 5586  (class class class)co 6282   |-> cmpt2 6284   omcom 6678   ~~ cen 7510   ~<_ cdom 7511   ~< csdm 7512   Fincfn 7513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-dc 8822

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-oadd 7131  df-er 7308  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517

This theorem is referenced by:  axcc  8834