axdc3lem2

Description: Lemma for axdc3 . We have constructed a "candidate set" S , which consists of all finite sequences s that satisfy our property of interest, namely s ( x + 1 ) e. F ( s ( x ) ) on its domain, but with the added constraint that s ( 0 ) = C . These sets are possible "initial segments" of theinfinite sequence satisfying these constraints, but we can leverage the standard ax-dc (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely ( hn ) : m --> A (for some integer m ). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence h , we can construct the sequence g that we are after. (Contributed by Mario Carneiro, 30-Jan-2013)

	Ref	Expression
Hypotheses	axdc3lem2.1	\|- A e. _V
	axdc3lem2.2	\|- S = { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
	axdc3lem2.3	\|- G = ( x e. S \|-> { y e. S \| ( dom y = suc dom x /\ ( y \|` dom x ) = x ) } )
Assertion	axdc3lem2	\|- ( E. h ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		axdc3lem2.1	\|- A e. _V
2		axdc3lem2.2	\|- S = { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
3		axdc3lem2.3	\|- G = ( x e. S \|-> { y e. S \| ( dom y = suc dom x /\ ( y \|` dom x ) = x ) } )
4		id	\|- ( m = (/) -> m = (/) )
5		fveq2	\|- ( m = (/) -> ( h ` m ) = ( h ` (/) ) )
6	5	dmeqd	\|- ( m = (/) -> dom ( h ` m ) = dom ( h ` (/) ) )
7	4 6	eleq12d	\|- ( m = (/) -> ( m e. dom ( h ` m ) <-> (/) e. dom ( h ` (/) ) ) )
8		eleq2	\|- ( m = (/) -> ( j e. m <-> j e. (/) ) )
9	5	sseq2d	\|- ( m = (/) -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` (/) ) ) )
10	8 9	imbi12d	\|- ( m = (/) -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
11	7 10	anbi12d	\|- ( m = (/) -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) ) )
12		id	\|- ( m = i -> m = i )
13		fveq2	\|- ( m = i -> ( h ` m ) = ( h ` i ) )
14	13	dmeqd	\|- ( m = i -> dom ( h ` m ) = dom ( h ` i ) )
15	12 14	eleq12d	\|- ( m = i -> ( m e. dom ( h ` m ) <-> i e. dom ( h ` i ) ) )
16		elequ2	\|- ( m = i -> ( j e. m <-> j e. i ) )
17	13	sseq2d	\|- ( m = i -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` i ) ) )
18	16 17	imbi12d	\|- ( m = i -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) )
19	15 18	anbi12d	\|- ( m = i -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) ) )
20		id	\|- ( m = suc i -> m = suc i )
21		fveq2	\|- ( m = suc i -> ( h ` m ) = ( h ` suc i ) )
22	21	dmeqd	\|- ( m = suc i -> dom ( h ` m ) = dom ( h ` suc i ) )
23	20 22	eleq12d	\|- ( m = suc i -> ( m e. dom ( h ` m ) <-> suc i e. dom ( h ` suc i ) ) )
24		eleq2	\|- ( m = suc i -> ( j e. m <-> j e. suc i ) )
25	21	sseq2d	\|- ( m = suc i -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` suc i ) ) )
26	24 25	imbi12d	\|- ( m = suc i -> ( ( j e. m -> ( h ` j ) C_ ( h ` m ) ) <-> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
27	23 26	anbi12d	\|- ( m = suc i -> ( ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) <-> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
28		peano1	\|- (/) e. _om
29		ffvelcdm	\|- ( ( h : _om --> S /\ (/) e. _om ) -> ( h ` (/) ) e. S )
30	28 29	mpan2	\|- ( h : _om --> S -> ( h ` (/) ) e. S )
31		fdm	\|- ( s : suc n --> A -> dom s = suc n )
32		nnord	\|- ( n e. _om -> Ord n )
33		0elsuc	\|- ( Ord n -> (/) e. suc n )
34	32 33	syl	\|- ( n e. _om -> (/) e. suc n )
35		peano2	\|- ( n e. _om -> suc n e. _om )
36		eleq2	\|- ( dom s = suc n -> ( (/) e. dom s <-> (/) e. suc n ) )
37		eleq1	\|- ( dom s = suc n -> ( dom s e. _om <-> suc n e. _om ) )
38	36 37	anbi12d	\|- ( dom s = suc n -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. suc n /\ suc n e. _om ) ) )
39	38	biimprcd	\|- ( ( (/) e. suc n /\ suc n e. _om ) -> ( dom s = suc n -> ( (/) e. dom s /\ dom s e. _om ) ) )
40	34 35 39	syl2anc	\|- ( n e. _om -> ( dom s = suc n -> ( (/) e. dom s /\ dom s e. _om ) ) )
41	31 40	syl5com	\|- ( s : suc n --> A -> ( n e. _om -> ( (/) e. dom s /\ dom s e. _om ) ) )
42	41	3ad2ant1	\|- ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( (/) e. dom s /\ dom s e. _om ) ) )
43	42	impcom	\|- ( ( n e. _om /\ ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) -> ( (/) e. dom s /\ dom s e. _om ) )
44	43	rexlimiva	\|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( (/) e. dom s /\ dom s e. _om ) )
45	44	ss2abi	\|- { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s \| ( (/) e. dom s /\ dom s e. _om ) }
46	2 45	eqsstri	\|- S C_ { s \| ( (/) e. dom s /\ dom s e. _om ) }
47	46	sseli	\|- ( ( h ` (/) ) e. S -> ( h ` (/) ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } )
48		fvex	\|- ( h ` (/) ) e. _V
49		dmeq	\|- ( s = ( h ` (/) ) -> dom s = dom ( h ` (/) ) )
50	49	eleq2d	\|- ( s = ( h ` (/) ) -> ( (/) e. dom s <-> (/) e. dom ( h ` (/) ) ) )
51	49	eleq1d	\|- ( s = ( h ` (/) ) -> ( dom s e. _om <-> dom ( h ` (/) ) e. _om ) )
52	50 51	anbi12d	\|- ( s = ( h ` (/) ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) ) )
53	48 52	elab	\|- ( ( h ` (/) ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) )
54	47 53	sylib	\|- ( ( h ` (/) ) e. S -> ( (/) e. dom ( h ` (/) ) /\ dom ( h ` (/) ) e. _om ) )
55	54	simpld	\|- ( ( h ` (/) ) e. S -> (/) e. dom ( h ` (/) ) )
56	30 55	syl	\|- ( h : _om --> S -> (/) e. dom ( h ` (/) ) )
57		noel	\|- -. j e. (/)
58	57	pm2.21i	\|- ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) )
59	56 58	jctir	\|- ( h : _om --> S -> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
60	59	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( (/) e. dom ( h ` (/) ) /\ ( j e. (/) -> ( h ` j ) C_ ( h ` (/) ) ) ) )
61		ffvelcdm	\|- ( ( h : _om --> S /\ i e. _om ) -> ( h ` i ) e. S )
62	61	ancoms	\|- ( ( i e. _om /\ h : _om --> S ) -> ( h ` i ) e. S )
63	62	adantrr	\|- ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` i ) e. S )
64		suceq	\|- ( k = i -> suc k = suc i )
65	64	fveq2d	\|- ( k = i -> ( h ` suc k ) = ( h ` suc i ) )
66		2fveq3	\|- ( k = i -> ( G ` ( h ` k ) ) = ( G ` ( h ` i ) ) )
67	65 66	eleq12d	\|- ( k = i -> ( ( h ` suc k ) e. ( G ` ( h ` k ) ) <-> ( h ` suc i ) e. ( G ` ( h ` i ) ) ) )
68	67	rspcva	\|- ( ( i e. _om /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` suc i ) e. ( G ` ( h ` i ) ) )
69	68	adantrl	\|- ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` suc i ) e. ( G ` ( h ` i ) ) )
70	46	sseli	\|- ( ( h ` i ) e. S -> ( h ` i ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } )
71		fvex	\|- ( h ` i ) e. _V
72		dmeq	\|- ( s = ( h ` i ) -> dom s = dom ( h ` i ) )
73	72	eleq2d	\|- ( s = ( h ` i ) -> ( (/) e. dom s <-> (/) e. dom ( h ` i ) ) )
74	72	eleq1d	\|- ( s = ( h ` i ) -> ( dom s e. _om <-> dom ( h ` i ) e. _om ) )
75	73 74	anbi12d	\|- ( s = ( h ` i ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) ) )
76	71 75	elab	\|- ( ( h ` i ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) )
77	70 76	sylib	\|- ( ( h ` i ) e. S -> ( (/) e. dom ( h ` i ) /\ dom ( h ` i ) e. _om ) )
78	77	simprd	\|- ( ( h ` i ) e. S -> dom ( h ` i ) e. _om )
79		nnord	\|- ( dom ( h ` i ) e. _om -> Ord dom ( h ` i ) )
80		ordsucelsuc	\|- ( Ord dom ( h ` i ) -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
81	78 79 80	3syl	\|- ( ( h ` i ) e. S -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
82	81	adantr	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) <-> suc i e. suc dom ( h ` i ) ) )
83		dmeq	\|- ( x = ( h ` i ) -> dom x = dom ( h ` i ) )
84		suceq	\|- ( dom x = dom ( h ` i ) -> suc dom x = suc dom ( h ` i ) )
85	83 84	syl	\|- ( x = ( h ` i ) -> suc dom x = suc dom ( h ` i ) )
86	85	eqeq2d	\|- ( x = ( h ` i ) -> ( dom y = suc dom x <-> dom y = suc dom ( h ` i ) ) )
87	83	reseq2d	\|- ( x = ( h ` i ) -> ( y \|` dom x ) = ( y \|` dom ( h ` i ) ) )
88		id	\|- ( x = ( h ` i ) -> x = ( h ` i ) )
89	87 88	eqeq12d	\|- ( x = ( h ` i ) -> ( ( y \|` dom x ) = x <-> ( y \|` dom ( h ` i ) ) = ( h ` i ) ) )
90	86 89	anbi12d	\|- ( x = ( h ` i ) -> ( ( dom y = suc dom x /\ ( y \|` dom x ) = x ) <-> ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) ) )
91	90	rabbidv	\|- ( x = ( h ` i ) -> { y e. S \| ( dom y = suc dom x /\ ( y \|` dom x ) = x ) } = { y e. S \| ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) } )
92	1 2	axdc3lem	\|- S e. _V
93	92	rabex	\|- { y e. S \| ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) } e. _V
94	91 3 93	fvmpt	\|- ( ( h ` i ) e. S -> ( G ` ( h ` i ) ) = { y e. S \| ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) } )
95	94	eleq2d	\|- ( ( h ` i ) e. S -> ( ( h ` suc i ) e. ( G ` ( h ` i ) ) <-> ( h ` suc i ) e. { y e. S \| ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) } ) )
96		dmeq	\|- ( y = ( h ` suc i ) -> dom y = dom ( h ` suc i ) )
97	96	eqeq1d	\|- ( y = ( h ` suc i ) -> ( dom y = suc dom ( h ` i ) <-> dom ( h ` suc i ) = suc dom ( h ` i ) ) )
98		reseq1	\|- ( y = ( h ` suc i ) -> ( y \|` dom ( h ` i ) ) = ( ( h ` suc i ) \|` dom ( h ` i ) ) )
99	98	eqeq1d	\|- ( y = ( h ` suc i ) -> ( ( y \|` dom ( h ` i ) ) = ( h ` i ) <-> ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) ) )
100	97 99	anbi12d	\|- ( y = ( h ` suc i ) -> ( ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) <-> ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) ) ) )
101	100	elrab	\|- ( ( h ` suc i ) e. { y e. S \| ( dom y = suc dom ( h ` i ) /\ ( y \|` dom ( h ` i ) ) = ( h ` i ) ) } <-> ( ( h ` suc i ) e. S /\ ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) ) ) )
102	95 101	bitrdi	\|- ( ( h ` i ) e. S -> ( ( h ` suc i ) e. ( G ` ( h ` i ) ) <-> ( ( h ` suc i ) e. S /\ ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) ) ) ) )
103	102	simplbda	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( dom ( h ` suc i ) = suc dom ( h ` i ) /\ ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) ) )
104	103	simpld	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> dom ( h ` suc i ) = suc dom ( h ` i ) )
105	104	eleq2d	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) <-> suc i e. suc dom ( h ` i ) ) )
106	82 105	bitr4d	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) <-> suc i e. dom ( h ` suc i ) ) )
107	106	biimpd	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( i e. dom ( h ` i ) -> suc i e. dom ( h ` suc i ) ) )
108	103	simprd	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) )
109		resss	\|- ( ( h ` suc i ) \|` dom ( h ` i ) ) C_ ( h ` suc i )
110		sseq1	\|- ( ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) -> ( ( ( h ` suc i ) \|` dom ( h ` i ) ) C_ ( h ` suc i ) <-> ( h ` i ) C_ ( h ` suc i ) ) )
111	109 110	mpbii	\|- ( ( ( h ` suc i ) \|` dom ( h ` i ) ) = ( h ` i ) -> ( h ` i ) C_ ( h ` suc i ) )
112		elsuci	\|- ( j e. suc i -> ( j e. i \/ j = i ) )
113		pm2.27	\|- ( j e. i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( h ` j ) C_ ( h ` i ) ) )
114		sstr2	\|- ( ( h ` j ) C_ ( h ` i ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) )
115	113 114	syl6	\|- ( j e. i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
116		fveq2	\|- ( j = i -> ( h ` j ) = ( h ` i ) )
117	116	sseq1d	\|- ( j = i -> ( ( h ` j ) C_ ( h ` suc i ) <-> ( h ` i ) C_ ( h ` suc i ) ) )
118	117	biimprd	\|- ( j = i -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) )
119	118	a1d	\|- ( j = i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
120	115 119	jaoi	\|- ( ( j e. i \/ j = i ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
121	112 120	syl	\|- ( j e. suc i -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( ( h ` i ) C_ ( h ` suc i ) -> ( h ` j ) C_ ( h ` suc i ) ) ) )
122	121	com13	\|- ( ( h ` i ) C_ ( h ` suc i ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
123	108 111 122	3syl	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( j e. i -> ( h ` j ) C_ ( h ` i ) ) -> ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) )
124	107 123	anim12d	\|- ( ( ( h ` i ) e. S /\ ( h ` suc i ) e. ( G ` ( h ` i ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
125	63 69 124	syl2anc	\|- ( ( i e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) )
126	125	ex	\|- ( i e. _om -> ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( i e. dom ( h ` i ) /\ ( j e. i -> ( h ` j ) C_ ( h ` i ) ) ) -> ( suc i e. dom ( h ` suc i ) /\ ( j e. suc i -> ( h ` j ) C_ ( h ` suc i ) ) ) ) ) )
127	11 19 27 60 126	finds2	\|- ( m e. _om -> ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) ) )
128	127	imp	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( m e. dom ( h ` m ) /\ ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) )
129	128	simprd	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( j e. m -> ( h ` j ) C_ ( h ` m ) ) )
130	129	expcom	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> ( j e. m -> ( h ` j ) C_ ( h ` m ) ) ) )
131	130	ralrimdv	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> A. j e. m ( h ` j ) C_ ( h ` m ) ) )
132	131	ralrimiv	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) )
133		frn	\|- ( h : _om --> S -> ran h C_ S )
134		ffun	\|- ( s : suc n --> A -> Fun s )
135	134	3ad2ant1	\|- ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> Fun s )
136	135	rexlimivw	\|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> Fun s )
137	136	ss2abi	\|- { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s \| Fun s }
138	2 137	eqsstri	\|- S C_ { s \| Fun s }
139	133 138	sstrdi	\|- ( h : _om --> S -> ran h C_ { s \| Fun s } )
140	139	sseld	\|- ( h : _om --> S -> ( u e. ran h -> u e. { s \| Fun s } ) )
141		vex	\|- u e. _V
142		funeq	\|- ( s = u -> ( Fun s <-> Fun u ) )
143	141 142	elab	\|- ( u e. { s \| Fun s } <-> Fun u )
144	140 143	imbitrdi	\|- ( h : _om --> S -> ( u e. ran h -> Fun u ) )
145	144	adantr	\|- ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> Fun u ) )
146		ffn	\|- ( h : _om --> S -> h Fn _om )
147		fvelrnb	\|- ( h Fn _om -> ( v e. ran h <-> E. b e. _om ( h ` b ) = v ) )
148		fvelrnb	\|- ( h Fn _om -> ( u e. ran h <-> E. a e. _om ( h ` a ) = u ) )
149		nnord	\|- ( a e. _om -> Ord a )
150		nnord	\|- ( b e. _om -> Ord b )
151	149 150	anim12i	\|- ( ( a e. _om /\ b e. _om ) -> ( Ord a /\ Ord b ) )
152		ordtri3or	\|- ( ( Ord a /\ Ord b ) -> ( a e. b \/ a = b \/ b e. a ) )
153		fveq2	\|- ( m = b -> ( h ` m ) = ( h ` b ) )
154	153	sseq2d	\|- ( m = b -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` b ) ) )
155	154	raleqbi1dv	\|- ( m = b -> ( A. j e. m ( h ` j ) C_ ( h ` m ) <-> A. j e. b ( h ` j ) C_ ( h ` b ) ) )
156	155	rspcv	\|- ( b e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> A. j e. b ( h ` j ) C_ ( h ` b ) ) )
157		fveq2	\|- ( j = a -> ( h ` j ) = ( h ` a ) )
158	157	sseq1d	\|- ( j = a -> ( ( h ` j ) C_ ( h ` b ) <-> ( h ` a ) C_ ( h ` b ) ) )
159	158	rspccv	\|- ( A. j e. b ( h ` j ) C_ ( h ` b ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) )
160	156 159	syl6	\|- ( b e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) ) )
161	160	adantl	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( h ` a ) C_ ( h ` b ) ) ) )
162	161	3imp	\|- ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ a e. b ) -> ( h ` a ) C_ ( h ` b ) )
163	162	orcd	\|- ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ a e. b ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
164	163	3exp	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( a e. b -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
165	164	com3r	\|- ( a e. b -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
166		fveq2	\|- ( a = b -> ( h ` a ) = ( h ` b ) )
167		eqimss	\|- ( ( h ` a ) = ( h ` b ) -> ( h ` a ) C_ ( h ` b ) )
168	167	orcd	\|- ( ( h ` a ) = ( h ` b ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
169	166 168	syl	\|- ( a = b -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
170	169	2a1d	\|- ( a = b -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
171		fveq2	\|- ( m = a -> ( h ` m ) = ( h ` a ) )
172	171	sseq2d	\|- ( m = a -> ( ( h ` j ) C_ ( h ` m ) <-> ( h ` j ) C_ ( h ` a ) ) )
173	172	raleqbi1dv	\|- ( m = a -> ( A. j e. m ( h ` j ) C_ ( h ` m ) <-> A. j e. a ( h ` j ) C_ ( h ` a ) ) )
174	173	rspcv	\|- ( a e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> A. j e. a ( h ` j ) C_ ( h ` a ) ) )
175		fveq2	\|- ( j = b -> ( h ` j ) = ( h ` b ) )
176	175	sseq1d	\|- ( j = b -> ( ( h ` j ) C_ ( h ` a ) <-> ( h ` b ) C_ ( h ` a ) ) )
177	176	rspccv	\|- ( A. j e. a ( h ` j ) C_ ( h ` a ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) )
178	174 177	syl6	\|- ( a e. _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) ) )
179	178	adantr	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( h ` b ) C_ ( h ` a ) ) ) )
180	179	3imp	\|- ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ b e. a ) -> ( h ` b ) C_ ( h ` a ) )
181	180	olcd	\|- ( ( ( a e. _om /\ b e. _om ) /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) /\ b e. a ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) )
182	181	3exp	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( b e. a -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
183	182	com3r	\|- ( b e. a -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
184	165 170 183	3jaoi	\|- ( ( a e. b \/ a = b \/ b e. a ) -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
185	152 184	syl	\|- ( ( Ord a /\ Ord b ) -> ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) ) )
186	151 185	mpcom	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) ) )
187		sseq12	\|- ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( h ` a ) C_ ( h ` b ) <-> u C_ v ) )
188		sseq12	\|- ( ( ( h ` b ) = v /\ ( h ` a ) = u ) -> ( ( h ` b ) C_ ( h ` a ) <-> v C_ u ) )
189	188	ancoms	\|- ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( h ` b ) C_ ( h ` a ) <-> v C_ u ) )
190	187 189	orbi12d	\|- ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) <-> ( u C_ v \/ v C_ u ) ) )
191	190	biimpcd	\|- ( ( ( h ` a ) C_ ( h ` b ) \/ ( h ` b ) C_ ( h ` a ) ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( u C_ v \/ v C_ u ) ) )
192	186 191	syl6	\|- ( ( a e. _om /\ b e. _om ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( u C_ v \/ v C_ u ) ) ) )
193	192	com23	\|- ( ( a e. _om /\ b e. _om ) -> ( ( ( h ` a ) = u /\ ( h ` b ) = v ) -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) )
194	193	exp4b	\|- ( a e. _om -> ( b e. _om -> ( ( h ` a ) = u -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) ) )
195	194	com23	\|- ( a e. _om -> ( ( h ` a ) = u -> ( b e. _om -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) ) )
196	195	rexlimiv	\|- ( E. a e. _om ( h ` a ) = u -> ( b e. _om -> ( ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
197	196	rexlimdv	\|- ( E. a e. _om ( h ` a ) = u -> ( E. b e. _om ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) )
198	148 197	biimtrdi	\|- ( h Fn _om -> ( u e. ran h -> ( E. b e. _om ( h ` b ) = v -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
199	198	com23	\|- ( h Fn _om -> ( E. b e. _om ( h ` b ) = v -> ( u e. ran h -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
200	147 199	sylbid	\|- ( h Fn _om -> ( v e. ran h -> ( u e. ran h -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u C_ v \/ v C_ u ) ) ) ) )
201	200	com24	\|- ( h Fn _om -> ( A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) -> ( u e. ran h -> ( v e. ran h -> ( u C_ v \/ v C_ u ) ) ) ) )
202	201	imp	\|- ( ( h Fn _om /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> ( v e. ran h -> ( u C_ v \/ v C_ u ) ) ) )
203	202	ralrimdv	\|- ( ( h Fn _om /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> A. v e. ran h ( u C_ v \/ v C_ u ) ) )
204	146 203	sylan	\|- ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> A. v e. ran h ( u C_ v \/ v C_ u ) ) )
205	145 204	jcad	\|- ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> ( u e. ran h -> ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) ) )
206	205	ralrimiv	\|- ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> A. u e. ran h ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) )
207		fununi	\|- ( A. u e. ran h ( Fun u /\ A. v e. ran h ( u C_ v \/ v C_ u ) ) -> Fun U. ran h )
208	206 207	syl	\|- ( ( h : _om --> S /\ A. m e. _om A. j e. m ( h ` j ) C_ ( h ` m ) ) -> Fun U. ran h )
209	132 208	syldan	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> Fun U. ran h )
210		vex	\|- m e. _V
211	210	eldm2	\|- ( m e. dom U. ran h <-> E. u <. m , u >. e. U. ran h )
212		eluni2	\|- ( <. m , u >. e. U. ran h <-> E. v e. ran h <. m , u >. e. v )
213	210 141	opeldm	\|- ( <. m , u >. e. v -> m e. dom v )
214	213	a1i	\|- ( h : _om --> S -> ( <. m , u >. e. v -> m e. dom v ) )
215	133 46	sstrdi	\|- ( h : _om --> S -> ran h C_ { s \| ( (/) e. dom s /\ dom s e. _om ) } )
216		ssel	\|- ( ran h C_ { s \| ( (/) e. dom s /\ dom s e. _om ) } -> ( v e. ran h -> v e. { s \| ( (/) e. dom s /\ dom s e. _om ) } ) )
217		vex	\|- v e. _V
218		dmeq	\|- ( s = v -> dom s = dom v )
219	218	eleq2d	\|- ( s = v -> ( (/) e. dom s <-> (/) e. dom v ) )
220	218	eleq1d	\|- ( s = v -> ( dom s e. _om <-> dom v e. _om ) )
221	219 220	anbi12d	\|- ( s = v -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom v /\ dom v e. _om ) ) )
222	217 221	elab	\|- ( v e. { s \| ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom v /\ dom v e. _om ) )
223	222	simprbi	\|- ( v e. { s \| ( (/) e. dom s /\ dom s e. _om ) } -> dom v e. _om )
224	216 223	syl6	\|- ( ran h C_ { s \| ( (/) e. dom s /\ dom s e. _om ) } -> ( v e. ran h -> dom v e. _om ) )
225	215 224	syl	\|- ( h : _om --> S -> ( v e. ran h -> dom v e. _om ) )
226	214 225	anim12d	\|- ( h : _om --> S -> ( ( <. m , u >. e. v /\ v e. ran h ) -> ( m e. dom v /\ dom v e. _om ) ) )
227		elnn	\|- ( ( m e. dom v /\ dom v e. _om ) -> m e. _om )
228	226 227	syl6	\|- ( h : _om --> S -> ( ( <. m , u >. e. v /\ v e. ran h ) -> m e. _om ) )
229	228	expcomd	\|- ( h : _om --> S -> ( v e. ran h -> ( <. m , u >. e. v -> m e. _om ) ) )
230	229	rexlimdv	\|- ( h : _om --> S -> ( E. v e. ran h <. m , u >. e. v -> m e. _om ) )
231	212 230	biimtrid	\|- ( h : _om --> S -> ( <. m , u >. e. U. ran h -> m e. _om ) )
232	231	exlimdv	\|- ( h : _om --> S -> ( E. u <. m , u >. e. U. ran h -> m e. _om ) )
233	211 232	biimtrid	\|- ( h : _om --> S -> ( m e. dom U. ran h -> m e. _om ) )
234	233	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom U. ran h -> m e. _om ) )
235		id	\|- ( m e. _om -> m e. _om )
236		fnfvelrn	\|- ( ( h Fn _om /\ m e. _om ) -> ( h ` m ) e. ran h )
237	146 235 236	syl2anr	\|- ( ( m e. _om /\ h : _om --> S ) -> ( h ` m ) e. ran h )
238	237	adantrr	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> ( h ` m ) e. ran h )
239	128	simpld	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. dom ( h ` m ) )
240		dmeq	\|- ( u = ( h ` m ) -> dom u = dom ( h ` m ) )
241	240	eliuni	\|- ( ( ( h ` m ) e. ran h /\ m e. dom ( h ` m ) ) -> m e. U_ u e. ran h dom u )
242	238 239 241	syl2anc	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. U_ u e. ran h dom u )
243		dmuni	\|- dom U. ran h = U_ u e. ran h dom u
244	242 243	eleqtrrdi	\|- ( ( m e. _om /\ ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) ) -> m e. dom U. ran h )
245	244	expcom	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> m e. dom U. ran h ) )
246	234 245	impbid	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. dom U. ran h <-> m e. _om ) )
247	246	eqrdv	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> dom U. ran h = _om )
248		rnuni	\|- ran U. ran h = U_ s e. ran h ran s
249		frn	\|- ( s : suc n --> A -> ran s C_ A )
250	249	3ad2ant1	\|- ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ran s C_ A )
251	250	rexlimivw	\|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ran s C_ A )
252	251	ss2abi	\|- { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s \| ran s C_ A }
253	2 252	eqsstri	\|- S C_ { s \| ran s C_ A }
254	133 253	sstrdi	\|- ( h : _om --> S -> ran h C_ { s \| ran s C_ A } )
255		ssel	\|- ( ran h C_ { s \| ran s C_ A } -> ( s e. ran h -> s e. { s \| ran s C_ A } ) )
256		abid	\|- ( s e. { s \| ran s C_ A } <-> ran s C_ A )
257	255 256	imbitrdi	\|- ( ran h C_ { s \| ran s C_ A } -> ( s e. ran h -> ran s C_ A ) )
258	254 257	syl	\|- ( h : _om --> S -> ( s e. ran h -> ran s C_ A ) )
259	258	ralrimiv	\|- ( h : _om --> S -> A. s e. ran h ran s C_ A )
260		iunss	\|- ( U_ s e. ran h ran s C_ A <-> A. s e. ran h ran s C_ A )
261	259 260	sylibr	\|- ( h : _om --> S -> U_ s e. ran h ran s C_ A )
262	248 261	eqsstrid	\|- ( h : _om --> S -> ran U. ran h C_ A )
263	262	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ran U. ran h C_ A )
264		df-fn	\|- ( U. ran h Fn _om <-> ( Fun U. ran h /\ dom U. ran h = _om ) )
265		df-f	\|- ( U. ran h : _om --> A <-> ( U. ran h Fn _om /\ ran U. ran h C_ A ) )
266	265	biimpri	\|- ( ( U. ran h Fn _om /\ ran U. ran h C_ A ) -> U. ran h : _om --> A )
267	264 266	sylanbr	\|- ( ( ( Fun U. ran h /\ dom U. ran h = _om ) /\ ran U. ran h C_ A ) -> U. ran h : _om --> A )
268	209 247 263 267	syl21anc	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> U. ran h : _om --> A )
269		fnfvelrn	\|- ( ( h Fn _om /\ (/) e. _om ) -> ( h ` (/) ) e. ran h )
270	146 28 269	sylancl	\|- ( h : _om --> S -> ( h ` (/) ) e. ran h )
271	270	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` (/) ) e. ran h )
272		elssuni	\|- ( ( h ` (/) ) e. ran h -> ( h ` (/) ) C_ U. ran h )
273	271 272	syl	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( h ` (/) ) C_ U. ran h )
274	56	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> (/) e. dom ( h ` (/) ) )
275		funssfv	\|- ( ( Fun U. ran h /\ ( h ` (/) ) C_ U. ran h /\ (/) e. dom ( h ` (/) ) ) -> ( U. ran h ` (/) ) = ( ( h ` (/) ) ` (/) ) )
276	209 273 274 275	syl3anc	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( U. ran h ` (/) ) = ( ( h ` (/) ) ` (/) ) )
277		simp2	\|- ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( s ` (/) ) = C )
278	277	rexlimivw	\|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( s ` (/) ) = C )
279	278	ss2abi	\|- { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s \| ( s ` (/) ) = C }
280	2 279	eqsstri	\|- S C_ { s \| ( s ` (/) ) = C }
281	133 280	sstrdi	\|- ( h : _om --> S -> ran h C_ { s \| ( s ` (/) ) = C } )
282		ssel	\|- ( ran h C_ { s \| ( s ` (/) ) = C } -> ( ( h ` (/) ) e. ran h -> ( h ` (/) ) e. { s \| ( s ` (/) ) = C } ) )
283		fveq1	\|- ( s = ( h ` (/) ) -> ( s ` (/) ) = ( ( h ` (/) ) ` (/) ) )
284	283	eqeq1d	\|- ( s = ( h ` (/) ) -> ( ( s ` (/) ) = C <-> ( ( h ` (/) ) ` (/) ) = C ) )
285	48 284	elab	\|- ( ( h ` (/) ) e. { s \| ( s ` (/) ) = C } <-> ( ( h ` (/) ) ` (/) ) = C )
286	282 285	imbitrdi	\|- ( ran h C_ { s \| ( s ` (/) ) = C } -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
287	281 286	syl	\|- ( h : _om --> S -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
288	287	adantr	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( h ` (/) ) e. ran h -> ( ( h ` (/) ) ` (/) ) = C ) )
289	271 288	mpd	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( ( h ` (/) ) ` (/) ) = C )
290	276 289	eqtrd	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( U. ran h ` (/) ) = C )
291		nfv	\|- F/ k h : _om --> S
292		nfra1	\|- F/ k A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) )
293	291 292	nfan	\|- F/ k ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) )
294	133	ad2antrr	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ran h C_ S )
295		peano2	\|- ( k e. _om -> suc k e. _om )
296		fnfvelrn	\|- ( ( h Fn _om /\ suc k e. _om ) -> ( h ` suc k ) e. ran h )
297	146 295 296	syl2an	\|- ( ( h : _om --> S /\ k e. _om ) -> ( h ` suc k ) e. ran h )
298	297	adantlr	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( h ` suc k ) e. ran h )
299	239	expcom	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( m e. _om -> m e. dom ( h ` m ) ) )
300	299	ralrimiv	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. m e. _om m e. dom ( h ` m ) )
301		id	\|- ( m = suc k -> m = suc k )
302		fveq2	\|- ( m = suc k -> ( h ` m ) = ( h ` suc k ) )
303	302	dmeqd	\|- ( m = suc k -> dom ( h ` m ) = dom ( h ` suc k ) )
304	301 303	eleq12d	\|- ( m = suc k -> ( m e. dom ( h ` m ) <-> suc k e. dom ( h ` suc k ) ) )
305	304	rspcv	\|- ( suc k e. _om -> ( A. m e. _om m e. dom ( h ` m ) -> suc k e. dom ( h ` suc k ) ) )
306	295 305	syl	\|- ( k e. _om -> ( A. m e. _om m e. dom ( h ` m ) -> suc k e. dom ( h ` suc k ) ) )
307	300 306	mpan9	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> suc k e. dom ( h ` suc k ) )
308		eleq2	\|- ( dom s = suc n -> ( suc k e. dom s <-> suc k e. suc n ) )
309	308	biimpa	\|- ( ( dom s = suc n /\ suc k e. dom s ) -> suc k e. suc n )
310	31 309	sylan	\|- ( ( s : suc n --> A /\ suc k e. dom s ) -> suc k e. suc n )
311		ordsucelsuc	\|- ( Ord n -> ( k e. n <-> suc k e. suc n ) )
312	32 311	syl	\|- ( n e. _om -> ( k e. n <-> suc k e. suc n ) )
313	312	biimprd	\|- ( n e. _om -> ( suc k e. suc n -> k e. n ) )
314		rsp	\|- ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( k e. n -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
315	313 314	syl9r	\|- ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( n e. _om -> ( suc k e. suc n -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
316	315	com13	\|- ( suc k e. suc n -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
317	310 316	syl	\|- ( ( s : suc n --> A /\ suc k e. dom s ) -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
318	317	ex	\|- ( s : suc n --> A -> ( suc k e. dom s -> ( n e. _om -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) ) )
319	318	com24	\|- ( s : suc n --> A -> ( A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) ) )
320	319	imp	\|- ( ( s : suc n --> A /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
321	320	3adant2	\|- ( ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( n e. _om -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
322	321	impcom	\|- ( ( n e. _om /\ ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
323	322	rexlimiva	\|- ( E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) -> ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
324	323	ss2abi	\|- { s \| E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } C_ { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
325	2 324	eqsstri	\|- S C_ { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
326		sstr	\|- ( ( ran h C_ S /\ S C_ { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } ) -> ran h C_ { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } )
327	325 326	mpan2	\|- ( ran h C_ S -> ran h C_ { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } )
328	327	sseld	\|- ( ran h C_ S -> ( ( h ` suc k ) e. ran h -> ( h ` suc k ) e. { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } ) )
329		fvex	\|- ( h ` suc k ) e. _V
330		dmeq	\|- ( s = ( h ` suc k ) -> dom s = dom ( h ` suc k ) )
331	330	eleq2d	\|- ( s = ( h ` suc k ) -> ( suc k e. dom s <-> suc k e. dom ( h ` suc k ) ) )
332		fveq1	\|- ( s = ( h ` suc k ) -> ( s ` suc k ) = ( ( h ` suc k ) ` suc k ) )
333		fveq1	\|- ( s = ( h ` suc k ) -> ( s ` k ) = ( ( h ` suc k ) ` k ) )
334	333	fveq2d	\|- ( s = ( h ` suc k ) -> ( F ` ( s ` k ) ) = ( F ` ( ( h ` suc k ) ` k ) ) )
335	332 334	eleq12d	\|- ( s = ( h ` suc k ) -> ( ( s ` suc k ) e. ( F ` ( s ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
336	331 335	imbi12d	\|- ( s = ( h ` suc k ) -> ( ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) <-> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) ) )
337	329 336	elab	\|- ( ( h ` suc k ) e. { s \| ( suc k e. dom s -> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) } <-> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
338	328 337	imbitrdi	\|- ( ran h C_ S -> ( ( h ` suc k ) e. ran h -> ( suc k e. dom ( h ` suc k ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) ) )
339	294 298 307 338	syl3c	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) )
340	209	adantr	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> Fun U. ran h )
341		elssuni	\|- ( ( h ` suc k ) e. ran h -> ( h ` suc k ) C_ U. ran h )
342	297 341	syl	\|- ( ( h : _om --> S /\ k e. _om ) -> ( h ` suc k ) C_ U. ran h )
343	342	adantlr	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( h ` suc k ) C_ U. ran h )
344		funssfv	\|- ( ( Fun U. ran h /\ ( h ` suc k ) C_ U. ran h /\ suc k e. dom ( h ` suc k ) ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
345	340 343 307 344	syl3anc	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
346	215	sseld	\|- ( h : _om --> S -> ( ( h ` suc k ) e. ran h -> ( h ` suc k ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } ) )
347	330	eleq2d	\|- ( s = ( h ` suc k ) -> ( (/) e. dom s <-> (/) e. dom ( h ` suc k ) ) )
348	330	eleq1d	\|- ( s = ( h ` suc k ) -> ( dom s e. _om <-> dom ( h ` suc k ) e. _om ) )
349	347 348	anbi12d	\|- ( s = ( h ` suc k ) -> ( ( (/) e. dom s /\ dom s e. _om ) <-> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
350	329 349	elab	\|- ( ( h ` suc k ) e. { s \| ( (/) e. dom s /\ dom s e. _om ) } <-> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) )
351	346 350	imbitrdi	\|- ( h : _om --> S -> ( ( h ` suc k ) e. ran h -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
352	351	adantr	\|- ( ( h : _om --> S /\ k e. _om ) -> ( ( h ` suc k ) e. ran h -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) ) )
353	297 352	mpd	\|- ( ( h : _om --> S /\ k e. _om ) -> ( (/) e. dom ( h ` suc k ) /\ dom ( h ` suc k ) e. _om ) )
354	353	simprd	\|- ( ( h : _om --> S /\ k e. _om ) -> dom ( h ` suc k ) e. _om )
355		nnord	\|- ( dom ( h ` suc k ) e. _om -> Ord dom ( h ` suc k ) )
356		ordtr	\|- ( Ord dom ( h ` suc k ) -> Tr dom ( h ` suc k ) )
357		trsuc	\|- ( ( Tr dom ( h ` suc k ) /\ suc k e. dom ( h ` suc k ) ) -> k e. dom ( h ` suc k ) )
358	357	ex	\|- ( Tr dom ( h ` suc k ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
359	354 355 356 358	4syl	\|- ( ( h : _om --> S /\ k e. _om ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
360	359	adantlr	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( suc k e. dom ( h ` suc k ) -> k e. dom ( h ` suc k ) ) )
361	307 360	mpd	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> k e. dom ( h ` suc k ) )
362		funssfv	\|- ( ( Fun U. ran h /\ ( h ` suc k ) C_ U. ran h /\ k e. dom ( h ` suc k ) ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
363	340 343 361 362	syl3anc	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
364		simpl	\|- ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) )
365		simpr	\|- ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) )
366	365	fveq2d	\|- ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( F ` ( U. ran h ` k ) ) = ( F ` ( ( h ` suc k ) ` k ) ) )
367	364 366	eleq12d	\|- ( ( ( U. ran h ` suc k ) = ( ( h ` suc k ) ` suc k ) /\ ( U. ran h ` k ) = ( ( h ` suc k ) ` k ) ) -> ( ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
368	345 363 367	syl2anc	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) <-> ( ( h ` suc k ) ` suc k ) e. ( F ` ( ( h ` suc k ) ` k ) ) ) )
369	339 368	mpbird	\|- ( ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) /\ k e. _om ) -> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) )
370	369	ex	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> ( k e. _om -> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
371	293 370	ralrimi	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) )
372		vex	\|- h e. _V
373	372	rnex	\|- ran h e. _V
374	373	uniex	\|- U. ran h e. _V
375		feq1	\|- ( g = U. ran h -> ( g : _om --> A <-> U. ran h : _om --> A ) )
376		fveq1	\|- ( g = U. ran h -> ( g ` (/) ) = ( U. ran h ` (/) ) )
377	376	eqeq1d	\|- ( g = U. ran h -> ( ( g ` (/) ) = C <-> ( U. ran h ` (/) ) = C ) )
378		fveq1	\|- ( g = U. ran h -> ( g ` suc k ) = ( U. ran h ` suc k ) )
379		fveq1	\|- ( g = U. ran h -> ( g ` k ) = ( U. ran h ` k ) )
380	379	fveq2d	\|- ( g = U. ran h -> ( F ` ( g ` k ) ) = ( F ` ( U. ran h ` k ) ) )
381	378 380	eleq12d	\|- ( g = U. ran h -> ( ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
382	381	ralbidv	\|- ( g = U. ran h -> ( A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) <-> A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) )
383	375 377 382	3anbi123d	\|- ( g = U. ran h -> ( ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) <-> ( U. ran h : _om --> A /\ ( U. ran h ` (/) ) = C /\ A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) ) )
384	374 383	spcev	\|- ( ( U. ran h : _om --> A /\ ( U. ran h ` (/) ) = C /\ A. k e. _om ( U. ran h ` suc k ) e. ( F ` ( U. ran h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
385	268 290 371 384	syl3anc	\|- ( ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )
386	385	exlimiv	\|- ( E. h ( h : _om --> S /\ A. k e. _om ( h ` suc k ) e. ( G ` ( h ` k ) ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Metamath Proof Explorer

Theorem axdc3lem2

Proof