Theorem axcclem 8894

Description: Lemma for axcc 8895. (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 7838	. . . . . . . 8 |- ( A ~< om -> A e. Fin )
2		axcclem.1	. . . . . . . . . 10 |- A = ( x \ { (/) } )
3	2	eleq1i 2498	. . . . . . . . 9 |- ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
4		undif1 3872	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
5		snfi 7660	. . . . . . . . . . . 12 |- { (/) } e. Fin
6		unfi 7847	. . . . . . . . . . . 12 |- ( ( ( x \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
7	5, 6	mpan2 675	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) e. Fin -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
8	4, 7	syl5eqelr 2512	. . . . . . . . . 10 |- ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
9		ssun1 3629	. . . . . . . . . 10 |- x C_ ( x u. { (/) } )
10		ssfi 7801	. . . . . . . . . 10 |- ( ( ( x u. { (/) } ) e. Fin /\ x C_ ( x u. { (/) } ) ) -> x e. Fin )
11	8, 9, 10	sylancl 666	. . . . . . . . 9 |- ( ( x \ { (/) } ) e. Fin -> x e. Fin )
12	3, 11	sylbi 198	. . . . . . . 8 |- ( A e. Fin -> x e. Fin )
13		dcomex 8884	. . . . . . . . . 10 |- om e. _V
14		isfiniteg 7840	. . . . . . . . . 10 |- ( om e. _V -> ( x e. Fin <-> x ~< om ) )
15	13, 14	ax-mp 5	. . . . . . . . 9 |- ( x e. Fin <-> x ~< om )
16		sdomnen 7608	. . . . . . . . 9 |- ( x ~< om -> -. x ~~ om )
17	15, 16	sylbi 198	. . . . . . . 8 |- ( x e. Fin -> -. x ~~ om )
18	1, 12, 17	3syl 18	. . . . . . 7 |- ( A ~< om -> -. x ~~ om )
19	18	con2i 123	. . . . . 6 |- ( x ~~ om -> -. A ~< om )
20		sdomentr 7715	. . . . . . 7 |- ( ( A ~< x /\ x ~~ om ) -> A ~< om )
21	20	expcom 436	. . . . . 6 |- ( x ~~ om -> ( A ~< x -> A ~< om ) )
22	19, 21	mtod 180	. . . . 5 |- ( x ~~ om -> -. A ~< x )
23		vex 3083	. . . . . 6 |- x e. _V
24		difss 3592	. . . . . . 7 |- ( x \ { (/) } ) C_ x
25	2, 24	eqsstri 3494	. . . . . 6 |- A C_ x
26		ssdomg 7625	. . . . . 6 |- ( x e. _V -> ( A C_ x -> A ~<_ x ) )
27	23, 25, 26	mp2 9	. . . . 5 |- A ~<_ x
28	22, 27	jctil 539	. . . 4 |- ( x ~~ om -> ( A ~<_ x /\ -. A ~< x ) )
29		bren2 7610	. . . 4 |- ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
30	28, 29	sylibr 215	. . 3 |- ( x ~~ om -> A ~~ x )
31		entr 7631	. . 3 |- ( ( A ~~ x /\ x ~~ om ) -> A ~~ om )
32	30, 31	mpancom 673	. 2 |- ( x ~~ om -> A ~~ om )
33		ensym 7628	. 2 |- ( A ~~ om -> om ~~ A )
34		bren 7589	. . 3 |- ( om ~~ A <-> E. f f : om -1-1-onto-> A )
35		f1of 5831	. . . . . . . 8 |- ( f : om -1-1-onto-> A -> f : om --> A )
36		peano1 6726	. . . . . . . 8 |- (/) e. om
37		ffvelrn 6035	. . . . . . . 8 |- ( ( f : om --> A /\ (/) e. om ) -> ( f ` (/) ) e. A )
38	35, 36, 37	sylancl 666	. . . . . . 7 |- ( f : om -1-1-onto-> A -> ( f ` (/) ) e. A )
39		eldifn 3588	. . . . . . . . 9 |- ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
40	39, 2	eleq2s 2527	. . . . . . . 8 |- ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
41		fvex 5891	. . . . . . . . . . 11 |- ( f ` (/) ) e. _V
42	41	elsnc 4022	. . . . . . . . . 10 |- ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
43	42	notbii 297	. . . . . . . . 9 |- ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
44		neq0 3772	. . . . . . . . 9 |- ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
45	43, 44	bitr2i 253	. . . . . . . 8 |- ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
46	40, 45	sylibr 215	. . . . . . 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 4224	. . . . . . . . . . 11 |- ( ( c e. ( f ` (/) ) /\ ( f ` (/) ) e. A ) -> c e. U. A )
49	38, 48	sylan2 476	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> c e. U. A )
50	35	ffvelrnda 6037	. . . . . . . . . . . . . 14 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> ( f ` n ) e. A )
51		difabs 3737	. . . . . . . . . . . . . . . . . 18 |- ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
52	2	difeq1i 3579	. . . . . . . . . . . . . . . . . 18 |- ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
53	51, 52, 2	3eqtr4i 2461	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) = A
54		pwuni 4652	. . . . . . . . . . . . . . . . . 18 |- A C_ ~P U. A
55		ssdif 3600	. . . . . . . . . . . . . . . . . 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 3495	. . . . . . . . . . . . . . . 16 |- A C_ ( ~P U. A \ { (/) } )
58	57	sseli 3460	. . . . . . . . . . . . . . 15 |- ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
59	58	ralrimivw 2837	. . . . . . . . . . . . . 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 2836	. . . . . . . . . . . 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 6874	. . . . . . . . . . . 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 199	. . . . . . . . . . 11 |- ( f : om -1-1-onto-> A -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
65	64	adantl 467	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
66		difexg 4572	. . . . . . . . . . . . . 14 |- ( x e. _V -> ( x \ { (/) } ) e. _V )
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 |- ( x \ { (/) } ) e. _V
68	2, 67	eqeltri 2503	. . . . . . . . . . . 12 |- A e. _V
69	68	uniex 6601	. . . . . . . . . . 11 |- U. A e. _V
70	69	axdc4 8893	. . . . . . . . . 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 665	. . . . . . . . 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 1003	. . . . . . . . . 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 1701	. . . . . . . . 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 435	. . . . . . 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 1770	. . . . . 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 37	. . . . 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 4012	. . . . . . . . . . 11 |- ( z e. { (/) } <-> z = (/) )
79	78	necon3bbii 2681	. . . . . . . . . 10 |- ( -. z e. { (/) } <-> z =/= (/) )
80	2	eleq2i 2499	. . . . . . . . . . . 12 |- ( z e. A <-> z e. ( x \ { (/) } ) )
81		eldif 3446	. . . . . . . . . . . 12 |- ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82	80, 81	bitri 252	. . . . . . . . . . 11 |- ( z e. A <-> ( z e. x /\ -. z e. { (/) } ) )
83	82	biimpri 209	. . . . . . . . . 10 |- ( ( z e. x /\ -. z e. { (/) } ) -> z e. A )
84	79, 83	sylan2br 478	. . . . . . . . 9 |- ( ( z e. x /\ z =/= (/) ) -> z e. A )
85		simpl 458	. . . . . . . . . . . 12 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> f : om -1-1-onto-> A )
86		f1ofo 5838	. . . . . . . . . . . . . 14 |- ( f : om -1-1-onto-> A -> f : om -onto-> A )
87		foelrn 6056	. . . . . . . . . . . . . 14 |- ( ( f : om -onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
88	86, 87	sylan 473	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
89		suceq 5507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> suc k = suc i )
90	89	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
91		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> k = i )
92		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> ( h ` k ) = ( h ` i ) )
93	91, 92	oveq12d 6323	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
94	90, 93	eleq12d 2501	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95	94	rspcv 3178	. . . . . . . . . . . . . . . . . . . . . . 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 1028	. . . . . . . . . . . . . . . . . . . . . 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 430	. . . . . . . . . . . . . . . . . . . . 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 1025	. . . . . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = ( f ` i ) <-> ( f ` i ) = z )
100		f1ocnvfv 6192	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
101	99, 100	syl5bi 220	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102	101	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
103	102	imp 430	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> ( `' f ` z ) = i )
104	103	eqcomd 2430	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105	104	3adant2 1024	. . . . . . . . . . . . . . . . . . . . . 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 5507	. . . . . . . . . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> i e. om )
110		ffvelrn 6035	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> ( h ` i ) e. U. A )
111		fveq2 5881	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = i -> ( f ` n ) = ( f ` i ) )
112		eqidd 2423	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
113		fvex 5891	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f ` i ) e. _V
114	111, 112, 62, 113	ovmpt2 6446	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( i e. om /\ ( h ` i ) e. U. A ) -> ( i F ( h ` i ) ) = ( f ` i ) )
115	109, 110, 114	syl2anc 665	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
116	115	3adant2 1024	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117	116	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . 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 2521	. . . . . . . . . . . . . . . . . . 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 6037	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
120	119	3adant1 1023	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
121	120	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . . . 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 2495	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
123	122	3ad2ant3 1028	. . . . . . . . . . . . . . . . . . . . 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 235	. . . . . . . . . . . . . . . . . . . 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 5881	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
126		suceq 5507	. . . . . . . . . . . . . . . . . . . . . . 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 5885	. . . . . . . . . . . . . . . . . . . . 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 5891	. . . . . . . . . . . . . . . . . . . . 21 |- ( h ` suc ( `' f ` z ) ) e. _V
131	128, 129, 130	fvmpt 5964	. . . . . . . . . . . . . . . . . . . 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 1007	. . . . . . . . . . . . . . . . . . 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 2522	. . . . . . . . . . . . . . . . . 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 1204	. . . . . . . . . . . . . . . . 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 82	. . . . . . . . . . . . . . . 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 1222	. . . . . . . . . . . . . . 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 89	. . . . . . . . . . . . . 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 2908	. . . . . . . . . . . . 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 42	. . . . . . . . . . 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 432	. . . . . . . . . 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 441	. . . . . . . . 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 33	. . . . . . . 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 437	. . . . . . 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 2834	. . . . . 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 5903	. . . . . . . . . . 11 |- ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
148	147	rgenw 2783	. . . . . . . . . 10 |- A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
149		eqid 2422	. . . . . . . . . . 11 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
150	149	fmpt 6058	. . . . . . . . . 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 211	. . . . . . . . 9 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
152		vex 3083	. . . . . . . . . . 11 |- h e. _V
153	152	rnex 6741	. . . . . . . . . 10 |- ran h e. _V
154		p0ex 4611	. . . . . . . . . 10 |- { (/) } e. _V
155	153, 154	unex 6603	. . . . . . . . 9 |- ( ran h u. { (/) } ) e. _V
156		fex2 6762	. . . . . . . . 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 1360	. . . . . . . 8 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
158	129, 157	eqeltri 2503	. . . . . . 7 |- G e. _V
159		fveq1 5880	. . . . . . . . . 10 |- ( g = G -> ( g ` z ) = ( G ` z ) )
160	159	eleq1d 2491	. . . . . . . . 9 |- ( g = G -> ( ( g ` z ) e. z <-> ( G ` z ) e. z ) )
161	160	imbi2d 317	. . . . . . . 8 |- ( g = G -> ( ( z =/= (/) -> ( g ` z ) e. z ) <-> ( z =/= (/) -> ( G ` z ) e. z ) ) )
162	161	ralbidv 2861	. . . . . . 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 3173	. . . . . 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 1774	. . . 4 |- ( f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166	165	exlimiv 1770	. . 3 |- ( E. f f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
167	34, 166	sylbi 198	. 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 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1657   e. wcel 1872   =/= wne 2614   A.wral 2771   E.wrex 2772   _Vcvv 3080   \ cdif 3433   u. cun 3434   C_ wss 3436   (/)c0 3761   ~Pcpw 3981   {csn 3998   U.cuni 4219   class class class wbr 4423   |-> cmpt 4482   X. cxp 4851   `'ccnv 4852   ran crn 4854   suc csuc 5444   -->wf 5597   -onto->wfo 5599   -1-1-onto->wf1o 5600   ` cfv 5601  (class class class)co 6305   |-> cmpt2 6307   omcom 6706   ~~ cen 7577   ~<_ cdom 7578   ~< csdm 7579   Fincfn 7580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6597  ax-dc 8883

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-reu 2778  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7039  df-recs 7101  df-rdg 7139  df-1o 7193  df-oadd 7197  df-er 7374  df-en 7581  df-dom 7582  df-sdom 7583  df-fin 7584

This theorem is referenced by:  axcc  8895