Theorem axcclem 8874

Description: Lemma for axcc 8875. (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 7816	. . . . . . . 8 |- ( A ~< om -> A e. Fin )
2		axcclem.1	. . . . . . . . . 10 |- A = ( x \ { (/) } )
3	2	eleq1i 2521	. . . . . . . . 9 |- ( A e. Fin <-> ( x \ { (/) } ) e. Fin )
4		undif1 3810	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) u. { (/) } ) = ( x u. { (/) } )
5		snfi 7637	. . . . . . . . . . . 12 |- { (/) } e. Fin
6		unfi 7825	. . . . . . . . . . . 12 |- ( ( ( x \ { (/) } ) e. Fin /\ { (/) } e. Fin ) -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
7	5, 6	mpan2 682	. . . . . . . . . . 11 |- ( ( x \ { (/) } ) e. Fin -> ( ( x \ { (/) } ) u. { (/) } ) e. Fin )
8	4, 7	syl5eqelr 2535	. . . . . . . . . 10 |- ( ( x \ { (/) } ) e. Fin -> ( x u. { (/) } ) e. Fin )
9		ssun1 3565	. . . . . . . . . 10 |- x C_ ( x u. { (/) } )
10		ssfi 7779	. . . . . . . . . 10 |- ( ( ( x u. { (/) } ) e. Fin /\ x C_ ( x u. { (/) } ) ) -> x e. Fin )
11	8, 9, 10	sylancl 673	. . . . . . . . 9 |- ( ( x \ { (/) } ) e. Fin -> x e. Fin )
12	3, 11	sylbi 200	. . . . . . . 8 |- ( A e. Fin -> x e. Fin )
13		dcomex 8864	. . . . . . . . . 10 |- om e. _V
14		isfiniteg 7818	. . . . . . . . . 10 |- ( om e. _V -> ( x e. Fin <-> x ~< om ) )
15	13, 14	ax-mp 5	. . . . . . . . 9 |- ( x e. Fin <-> x ~< om )
16		sdomnen 7585	. . . . . . . . 9 |- ( x ~< om -> -. x ~~ om )
17	15, 16	sylbi 200	. . . . . . . 8 |- ( x e. Fin -> -. x ~~ om )
18	1, 12, 17	3syl 18	. . . . . . 7 |- ( A ~< om -> -. x ~~ om )
19	18	con2i 125	. . . . . 6 |- ( x ~~ om -> -. A ~< om )
20		sdomentr 7693	. . . . . . 7 |- ( ( A ~< x /\ x ~~ om ) -> A ~< om )
21	20	expcom 441	. . . . . 6 |- ( x ~~ om -> ( A ~< x -> A ~< om ) )
22	19, 21	mtod 182	. . . . 5 |- ( x ~~ om -> -. A ~< x )
23		vex 3016	. . . . . 6 |- x e. _V
24		difss 3528	. . . . . . 7 |- ( x \ { (/) } ) C_ x
25	2, 24	eqsstri 3430	. . . . . 6 |- A C_ x
26		ssdomg 7602	. . . . . 6 |- ( x e. _V -> ( A C_ x -> A ~<_ x ) )
27	23, 25, 26	mp2 9	. . . . 5 |- A ~<_ x
28	22, 27	jctil 544	. . . 4 |- ( x ~~ om -> ( A ~<_ x /\ -. A ~< x ) )
29		bren2 7587	. . . 4 |- ( A ~~ x <-> ( A ~<_ x /\ -. A ~< x ) )
30	28, 29	sylibr 217	. . 3 |- ( x ~~ om -> A ~~ x )
31		entr 7608	. . 3 |- ( ( A ~~ x /\ x ~~ om ) -> A ~~ om )
32	30, 31	mpancom 680	. 2 |- ( x ~~ om -> A ~~ om )
33		ensym 7605	. 2 |- ( A ~~ om -> om ~~ A )
34		bren 7565	. . 3 |- ( om ~~ A <-> E. f f : om -1-1-onto-> A )
35		f1of 5797	. . . . . . . 8 |- ( f : om -1-1-onto-> A -> f : om --> A )
36		peano1 6700	. . . . . . . 8 |- (/) e. om
37		ffvelrn 6004	. . . . . . . 8 |- ( ( f : om --> A /\ (/) e. om ) -> ( f ` (/) ) e. A )
38	35, 36, 37	sylancl 673	. . . . . . 7 |- ( f : om -1-1-onto-> A -> ( f ` (/) ) e. A )
39		eldifn 3524	. . . . . . . . 9 |- ( ( f ` (/) ) e. ( x \ { (/) } ) -> -. ( f ` (/) ) e. { (/) } )
40	39, 2	eleq2s 2548	. . . . . . . 8 |- ( ( f ` (/) ) e. A -> -. ( f ` (/) ) e. { (/) } )
41		fvex 5858	. . . . . . . . . . 11 |- ( f ` (/) ) e. _V
42	41	elsnc 3960	. . . . . . . . . 10 |- ( ( f ` (/) ) e. { (/) } <-> ( f ` (/) ) = (/) )
43	42	notbii 302	. . . . . . . . 9 |- ( -. ( f ` (/) ) e. { (/) } <-> -. ( f ` (/) ) = (/) )
44		neq0 3710	. . . . . . . . 9 |- ( -. ( f ` (/) ) = (/) <-> E. c c e. ( f ` (/) ) )
45	43, 44	bitr2i 258	. . . . . . . 8 |- ( E. c c e. ( f ` (/) ) <-> -. ( f ` (/) ) e. { (/) } )
46	40, 45	sylibr 217	. . . . . . 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 4173	. . . . . . . . . . 11 |- ( ( c e. ( f ` (/) ) /\ ( f ` (/) ) e. A ) -> c e. U. A )
49	38, 48	sylan2 481	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> c e. U. A )
50	35	ffvelrnda 6006	. . . . . . . . . . . . . 14 |- ( ( f : om -1-1-onto-> A /\ n e. om ) -> ( f ` n ) e. A )
51		difabs 3675	. . . . . . . . . . . . . . . . . 18 |- ( ( x \ { (/) } ) \ { (/) } ) = ( x \ { (/) } )
52	2	difeq1i 3515	. . . . . . . . . . . . . . . . . 18 |- ( A \ { (/) } ) = ( ( x \ { (/) } ) \ { (/) } )
53	51, 52, 2	3eqtr4i 2484	. . . . . . . . . . . . . . . . 17 |- ( A \ { (/) } ) = A
54		pwuni 4604	. . . . . . . . . . . . . . . . . 18 |- A C_ ~P U. A
55		ssdif 3536	. . . . . . . . . . . . . . . . . 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 3431	. . . . . . . . . . . . . . . 16 |- A C_ ( ~P U. A \ { (/) } )
58	57	sseli 3396	. . . . . . . . . . . . . . 15 |- ( ( f ` n ) e. A -> ( f ` n ) e. ( ~P U. A \ { (/) } ) )
59	58	ralrimivw 2791	. . . . . . . . . . . . . 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 2790	. . . . . . . . . . . 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 201	. . . . . . . . . . 11 |- ( f : om -1-1-onto-> A -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
65	64	adantl 472	. . . . . . . . . 10 |- ( ( c e. ( f ` (/) ) /\ f : om -1-1-onto-> A ) -> F : ( om X. U. A ) --> ( ~P U. A \ { (/) } ) )
66		difexg 4524	. . . . . . . . . . . . . 14 |- ( x e. _V -> ( x \ { (/) } ) e. _V )
67	23, 66	ax-mp 5	. . . . . . . . . . . . 13 |- ( x \ { (/) } ) e. _V
68	2, 67	eqeltri 2526	. . . . . . . . . . . 12 |- A e. _V
69	68	uniex 6575	. . . . . . . . . . 11 |- U. A e. _V
70	69	axdc4 8873	. . . . . . . . . 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 671	. . . . . . . . 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 1007	. . . . . . . . . 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 1711	. . . . . . . . 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 440	. . . . . . 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 1780	. . . . . 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 3950	. . . . . . . . . . 11 |- ( z e. { (/) } <-> z = (/) )
79	78	necon3bbii 2671	. . . . . . . . . 10 |- ( -. z e. { (/) } <-> z =/= (/) )
80	2	eleq2i 2522	. . . . . . . . . . . 12 |- ( z e. A <-> z e. ( x \ { (/) } ) )
81		eldif 3382	. . . . . . . . . . . 12 |- ( z e. ( x \ { (/) } ) <-> ( z e. x /\ -. z e. { (/) } ) )
82	80, 81	bitri 257	. . . . . . . . . . 11 |- ( z e. A <-> ( z e. x /\ -. z e. { (/) } ) )
83	82	biimpri 211	. . . . . . . . . 10 |- ( ( z e. x /\ -. z e. { (/) } ) -> z e. A )
84	79, 83	sylan2br 483	. . . . . . . . 9 |- ( ( z e. x /\ z =/= (/) ) -> z e. A )
85		simpl 463	. . . . . . . . . . . 12 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> f : om -1-1-onto-> A )
86		f1ofo 5804	. . . . . . . . . . . . . 14 |- ( f : om -1-1-onto-> A -> f : om -onto-> A )
87		foelrn 6025	. . . . . . . . . . . . . 14 |- ( ( f : om -onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
88	86, 87	sylan 478	. . . . . . . . . . . . 13 |- ( ( f : om -1-1-onto-> A /\ z e. A ) -> E. i e. om z = ( f ` i ) )
89		suceq 5467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> suc k = suc i )
90	89	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
91		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> k = i )
92		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = i -> ( h ` k ) = ( h ` i ) )
93	91, 92	oveq12d 6294	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = i -> ( k F ( h ` k ) ) = ( i F ( h ` i ) ) )
94	90, 93	eleq12d 2524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = i -> ( ( h ` suc k ) e. ( k F ( h ` k ) ) <-> ( h ` suc i ) e. ( i F ( h ` i ) ) ) )
95	94	rspcv 3114	. . . . . . . . . . . . . . . . . . . . . . 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 1032	. . . . . . . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . . . . . . 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 1029	. . . . . . . . . . . . . . . . . . . 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 2459	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( z = ( f ` i ) <-> ( f ` i ) = z )
100		f1ocnvfv 6163	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( ( f ` i ) = z -> ( `' f ` z ) = i ) )
101	99, 100	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
102	101	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( z = ( f ` i ) -> ( `' f ` z ) = i ) )
103	102	imp 435	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> ( `' f ` z ) = i )
104	103	eqcomd 2458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
105	104	3adant2 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 ) ) /\ z = ( f ` i ) ) -> i = ( `' f ` z ) )
106		suceq 5467	. . . . . . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . . . . 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 467	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> i e. om )
110		ffvelrn 6004	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( h : om --> U. A /\ i e. om ) -> ( h ` i ) e. U. A )
111		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n = i -> ( f ` n ) = ( f ` i ) )
112		eqidd 2453	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y = ( h ` i ) -> ( f ` i ) = ( f ` i ) )
113		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . 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 671	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
116	115	3adant2 1028	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( i F ( h ` i ) ) = ( f ` i ) )
117	116	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . 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 2544	. . . . . . . . . . . . . . . . . . 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 6006	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
120	119	3adant1 1027	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( h : om --> U. A /\ f : om -1-1-onto-> A /\ i e. om ) -> ( f ` i ) e. A )
121	120	3ad2ant1 1030	. . . . . . . . . . . . . . . . . . . . 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 2518	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z = ( f ` i ) -> ( z e. A <-> ( f ` i ) e. A ) )
123	122	3ad2ant3 1032	. . . . . . . . . . . . . . . . . . . . 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 240	. . . . . . . . . . . . . . . . . . . 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 5848	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( w = z -> ( `' f ` w ) = ( `' f ` z ) )
126		suceq 5467	. . . . . . . . . . . . . . . . . . . . . . 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 5852	. . . . . . . . . . . . . . . . . . . . 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 5858	. . . . . . . . . . . . . . . . . . . . 21 |- ( h ` suc ( `' f ` z ) ) e. _V
131	128, 129, 130	fvmpt 5932	. . . . . . . . . . . . . . . . . . . 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 1011	. . . . . . . . . . . . . . . . . . 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 2545	. . . . . . . . . . . . . . . . . 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 1209	. . . . . . . . . . . . . . . . 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 1229	. . . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . 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 437	. . . . . . . . . 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 446	. . . . . . . . 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 442	. . . . . . 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 2789	. . . . . 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 5870	. . . . . . . . . . 11 |- ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
148	147	rgenw 2749	. . . . . . . . . 10 |- A. w e. A ( h ` suc ( `' f ` w ) ) e. ( ran h u. { (/) } )
149		eqid 2452	. . . . . . . . . . 11 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) = ( w e. A |-> ( h ` suc ( `' f ` w ) ) )
150	149	fmpt 6027	. . . . . . . . . 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 213	. . . . . . . . 9 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) : A --> ( ran h u. { (/) } )
152		vex 3016	. . . . . . . . . . 11 |- h e. _V
153	152	rnex 6715	. . . . . . . . . 10 |- ran h e. _V
154		p0ex 4563	. . . . . . . . . 10 |- { (/) } e. _V
155	153, 154	unex 6577	. . . . . . . . 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 1368	. . . . . . . 8 |- ( w e. A |-> ( h ` suc ( `' f ` w ) ) ) e. _V
158	129, 157	eqeltri 2526	. . . . . . 7 |- G e. _V
159		fveq1 5847	. . . . . . . . . 10 |- ( g = G -> ( g ` z ) = ( G ` z ) )
160	159	eleq1d 2514	. . . . . . . . 9 |- ( g = G -> ( ( g ` z ) e. z <-> ( G ` z ) e. z ) )
161	160	imbi2d 322	. . . . . . . 8 |- ( g = G -> ( ( z =/= (/) -> ( g ` z ) e. z ) <-> ( z =/= (/) -> ( G ` z ) e. z ) ) )
162	161	ralbidv 2810	. . . . . . 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 3109	. . . . . 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 1785	. . . 4 |- ( f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
166	165	exlimiv 1780	. . 3 |- ( E. f f : om -1-1-onto-> A -> E. g A. z e. x ( z =/= (/) -> ( g ` z ) e. z ) )
167	34, 166	sylbi 200	. 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 189   /\ wa 375   /\ w3a 986   = wceq 1448   E.wex 1667   e. wcel 1891   =/= wne 2622   A.wral 2737   E.wrex 2738   _Vcvv 3013   \ cdif 3369   u. cun 3370   C_ wss 3372   (/)c0 3699   ~Pcpw 3919   {csn 3936   U.cuni 4168   class class class wbr 4374   |-> cmpt 4433   X. cxp 4810   `'ccnv 4811   ran crn 4813   suc csuc 5404   -->wf 5557   -onto->wfo 5559   -1-1-onto->wf1o 5560   ` cfv 5561  (class class class)co 6276   |-> cmpt2 6278   omcom 6680   ~~ 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 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571  ax-dc 8863

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-int 4205  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-ov 6279  df-oprab 6280  df-mpt2 6281  df-om 6681  df-1st 6781  df-2nd 6782  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  8875