MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axdc3lem2 Unicode version

Theorem axdc3lem2 8093
Description: Lemma for axdc3 8096. 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 the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 8088 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely  ( h `  n ) : 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 8088 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.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) ) ) )
Distinct variable groups:    A, g, h    A, n, s    C, g, h, k    C, n, s, k    g, F, h    n, F, s   
k, G    S, k,
s    x, S, y    h, s    x, h, y
Allowed substitution hints:    A( x, y, k)    C( x, y)    S( g, h, n)    F( x, y, k)    G( x, y, g, h, n, s)

Proof of Theorem axdc3lem2
Dummy variables  i 
j  m  u  v  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 19 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  m  =  (/) )
2 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
32dmeqd 4897 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  dom  (
h `  m )  =  dom  ( h `  (/) ) )
41, 3eleq12d 2364 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( m  e.  dom  ( h `
 m )  <->  (/)  e.  dom  ( h `  (/) ) ) )
5 eleq2 2357 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( j  e.  m  <->  j  e.  (/) ) )
62sseq2d 3219 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( ( h `  j ) 
C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  (/) ) ) )
75, 6imbi12d 311 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( ( j  e.  m  -> 
( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) ) ) )
84, 7anbi12d 691 . . . . . . . . . . 11  |-  ( m  =  (/)  ->  ( ( m  e.  dom  (
h `  m )  /\  ( j  e.  m  ->  ( h `  j
)  C_  ( h `  m ) ) )  <-> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) ) )
9 id 19 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  m  =  i )
10 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
1110dmeqd 4897 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  dom  ( h `  m
)  =  dom  (
h `  i )
)
129, 11eleq12d 2364 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
m  e.  dom  (
h `  m )  <->  i  e.  dom  ( h `
 i ) ) )
13 elequ2 1701 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
j  e.  m  <->  j  e.  i ) )
1410sseq2d 3219 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  i )
) )
1513, 14imbi12d 311 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
( j  e.  m  ->  ( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  i  ->  ( h `
 j )  C_  ( h `  i
) ) ) )
1612, 15anbi12d 691 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
17 id 19 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  m  =  suc  i )
18 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
1918dmeqd 4897 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  dom  ( h `  m
)  =  dom  (
h `  suc  i ) )
2017, 19eleq12d 2364 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( m  e.  dom  ( h `  m
)  <->  suc  i  e.  dom  ( h `  suc  i ) ) )
21 eleq2 2357 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( j  e.  m  <->  j  e.  suc  i ) )
2218sseq2d 3219 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( ( h `  j )  C_  (
h `  m )  <->  ( h `  j ) 
C_  ( h `  suc  i ) ) )
2321, 22imbi12d 311 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( ( j  e.  m  ->  ( h `  j )  C_  (
h `  m )
)  <->  ( j  e. 
suc  i  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
2420, 23anbi12d 691 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
25 peano1 4691 . . . . . . . . . . . . . . 15  |-  (/)  e.  om
26 ffvelrn 5679 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  (/) 
e.  om )  ->  (
h `  (/) )  e.  S )
2725, 26mpan2 652 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( h `  (/) )  e.  S )
28 axdc3lem2.2 . . . . . . . . . . . . . . . . . 18  |-  S  =  { s  |  E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) ) }
29 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s : suc  n --> A  ->  dom  s  =  suc  n )
30 nnord 4680 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  om  ->  Ord  n )
31 0elsuc 4642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord  n  ->  (/)  e.  suc  n )
3230, 31syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  (/)  e.  suc  n )
33 peano2 4692 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  suc  n  e.  om )
34 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s 
<->  (/)  e.  suc  n ) )
35 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( dom  s  e. 
om 
<->  suc  n  e.  om ) )
3634, 35anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  s  =  suc  n  ->  ( ( (/)  e.  dom  s  /\  dom  s  e. 
om )  <->  ( (/)  e.  suc  n  /\  suc  n  e. 
om ) ) )
3736biimprcd 216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
(/)  e.  suc  n  /\  suc  n  e.  om )  ->  ( dom  s  =  suc  n  ->  ( (/) 
e.  dom  s  /\  dom  s  e.  om ) ) )
3832, 33, 37syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  om  ->  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
3929, 38syl5com 26 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s : suc  n --> A  -> 
( n  e.  om  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
40393ad2ant1 976 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) ) )
4140impcom 419 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) )
4241rexlimiva 2675 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) )
4342ss2abi 3258 . . . . . . . . . . . . . . . . . 18  |-  { 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 ) }
4428, 43eqsstri 3221 . . . . . . . . . . . . . . . . 17  |-  S  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) }
4544sseli 3189 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e.  S  ->  ( h `  (/) )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } )
46 fvex 5555 . . . . . . . . . . . . . . . . 17  |-  ( h `
 (/) )  e.  _V
47 dmeq 4895 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  ( h `  (/) )  ->  dom  s  =  dom  ( h `  (/) ) )
4847eleq2d 2363 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( (/)  e.  dom  s 
<->  (/)  e.  dom  ( h `
 (/) ) ) )
4947eleq1d 2362 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( dom  s  e.  om  <->  dom  ( h `
 (/) )  e.  om ) )
5048, 49anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  (/) )  ->  ( ( (/) 
e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) ) )
5146, 50elab 2927 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e. 
{ s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) }  <->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5245, 51sylib 188 . . . . . . . . . . . . . . 15  |-  ( ( h `  (/) )  e.  S  ->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5352simpld 445 . . . . . . . . . . . . . 14  |-  ( ( h `  (/) )  e.  S  ->  (/)  e.  dom  ( h `  (/) ) )
5427, 53syl 15 . . . . . . . . . . . . 13  |-  ( h : om --> S  ->  (/) 
e.  dom  ( h `  (/) ) )
55 noel 3472 . . . . . . . . . . . . . 14  |-  -.  j  e.  (/)
5655pm2.21i 123 . . . . . . . . . . . . 13  |-  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) )
5754, 56jctir 524 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) )
5857adantr 451 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) )
59 ffvelrn 5679 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  i  e.  om )  ->  ( h `  i
)  e.  S )
6059ancoms 439 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  h : om --> S )  ->  ( h `  i )  e.  S
)
6160adantrr 697 . . . . . . . . . . . . 13  |-  ( ( i  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
h `  i )  e.  S )
62 suceq 4473 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  suc  k  =  suc  i )
6362fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
64 fveq2 5541 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
6564fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
6663, 65eleq12d 2364 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
6766rspcva 2895 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )
6867adantrl 696 . . . . . . . . . . . . 13  |-  ( ( i  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
h `  suc  i )  e.  ( G `  ( h `  i
) ) )
6944sseli 3189 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  S  ->  (
h `  i )  e.  { s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) } )
70 fvex 5555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h `
 i )  e. 
_V
71 dmeq 4895 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( h `  i )  ->  dom  s  =  dom  ( h `
 i ) )
7271eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  i
) ) )
7371eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( dom  s  e.  om  <->  dom  ( h `  i
)  e.  om )
)
7472, 73anbi12d 691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( h `  i )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) ) )
7570, 74elab 2927 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) )
7669, 75sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  i )  e.  S  ->  ( (/) 
e.  dom  ( h `  i )  /\  dom  ( h `  i
)  e.  om )
)
7776simprd 449 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  i )  e.  S  ->  dom  ( h `  i
)  e.  om )
78 nnord 4680 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( h `  i
)  e.  om  ->  Ord 
dom  ( h `  i ) )
79 ordsucelsuc 4629 . . . . . . . . . . . . . . . . . 18  |-  ( Ord 
dom  ( h `  i )  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8077, 78, 793syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  i )  e.  S  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8180adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( i  e.  dom  ( h `  i )  <->  suc  i  e. 
suc  dom  ( h `  i ) ) )
82 dmeq 4895 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( h `  i )  ->  dom  x  =  dom  ( h `
 i ) )
83 suceq 4473 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  x  =  dom  (
h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i ) )
8482, 83syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i
) )
8584eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  ( dom  y  =  suc  dom  x  <->  dom  y  =  suc  dom  ( h `  i
) ) )
8682reseq2d 4971 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  (
y  |`  dom  x )  =  ( y  |`  dom  ( h `  i
) ) )
87 id 19 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  x  =  ( h `  i ) )
8886, 87eqeq12d 2310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  (
( y  |`  dom  x
)  =  x  <->  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) )
8985, 88anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( x  =  ( h `  i )  ->  (
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x )  <->  ( dom  y  =  suc  dom  (
h `  i )  /\  ( y  |`  dom  (
h `  i )
)  =  ( h `
 i ) ) ) )
9089rabbidv 2793 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) } )
91 axdc3lem2.3 . . . . . . . . . . . . . . . . . . . . . 22  |-  G  =  ( x  e.  S  |->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) } )
92 axdc3lem2.1 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  A  e. 
_V
9392, 28axdc3lem 8092 . . . . . . . . . . . . . . . . . . . . . . 23  |-  S  e. 
_V
9493rabex 4181 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i
)  /\  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) }  e.  _V
9590, 91, 94fvmpt 5618 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  i )  e.  S  ->  ( G `  ( h `  i ) )  =  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i )  /\  (
y  |`  dom  ( h `
 i ) )  =  ( h `  i ) ) } )
9695eleq2d 2363 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) } ) )
97 dmeq 4895 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  dom  y  =  dom  ( h `
 suc  i )
)
9897eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  ( dom  y  =  suc  dom  ( h `  i
)  <->  dom  ( h `  suc  i )  =  suc  dom  ( h `  i
) ) )
99 reseq1 4965 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  (
y  |`  dom  ( h `
 i ) )  =  ( ( h `
 suc  i )  |` 
dom  ( h `  i ) ) )
10099eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  (
( y  |`  dom  (
h `  i )
)  =  ( h `
 i )  <->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) ) )
10198, 100anbi12d 691 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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
) ) ) )
102101elrab 2936 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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
) ) ) )
10396, 102syl6bb 252 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) ) )
104103simplbda 607 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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
) ) )
105104simpld 445 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  dom  ( h `
 suc  i )  =  suc  dom  ( h `  i ) )
106105eleq2d 2363 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
10781, 106bitr4d 247 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( i  e.  dom  ( h `  i )  <->  suc  i  e. 
dom  ( h `  suc  i ) ) )
108107biimpd 198 . . . . . . . . . . . . . 14  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( i  e.  dom  ( h `  i )  ->  suc  i  e.  dom  ( h `
 suc  i )
) )
109104simprd 449 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) )
110 resss 4995 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  i
)  |`  dom  ( h `
 i ) ) 
C_  ( h `  suc  i )
111 sseq1 3212 . . . . . . . . . . . . . . . 16  |-  ( ( ( h `  suc  i )  |`  dom  (
h `  i )
)  =  ( h `
 i )  -> 
( ( ( h `
 suc  i )  |` 
dom  ( h `  i ) )  C_  ( h `  suc  i )  <->  ( h `  i )  C_  (
h `  suc  i ) ) )
112110, 111mpbii 202 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  suc  i )  |`  dom  (
h `  i )
)  =  ( h `
 i )  -> 
( h `  i
)  C_  ( h `  suc  i ) )
113 elsuci 4474 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  suc  i  -> 
( j  e.  i  \/  j  =  i ) )
114 pm2.27 35 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( h `  j )  C_  (
h `  i )
) )
115 sstr2 3199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  j ) 
C_  ( h `  i )  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
116114, 115syl6 29 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( (
h `  i )  C_  ( h `  suc  i )  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
117 fveq2 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  (
h `  j )  =  ( h `  i ) )
118117sseq1d 3218 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
( h `  j
)  C_  ( h `  suc  i )  <->  ( h `  i )  C_  (
h `  suc  i ) ) )
119118biimprd 214 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
120119a1d 22 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( (
h `  i )  C_  ( h `  suc  i )  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
121116, 120jaoi 368 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) ) )
122113, 121syl 15 . . . . . . . . . . . . . . . 16  |-  ( j  e.  suc  i  -> 
( ( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( (
h `  i )  C_  ( h `  suc  i )  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
123122com13 74 . . . . . . . . . . . . . . 15  |-  ( ( h `  i ) 
C_  ( h `  suc  i )  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( j  e.  suc  i  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
124109, 112, 1233syl 18 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
125108, 124anim12d 546 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) ) ) )
12661, 68, 125syl2anc 642 . . . . . . . . . . . 12  |-  ( ( 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 ) ) ) ) )
127126ex 423 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) ) )
1288, 16, 24, 58, 127finds2 4700 . . . . . . . . . 10  |-  ( 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 ) ) ) ) )
129128imp 418 . . . . . . . . 9  |-  ( ( 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 ) ) ) )
130129simprd 449 . . . . . . . 8  |-  ( ( 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 ) ) )
131130expcom 424 . . . . . . 7  |-  ( ( 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 ) ) ) )
132131ralrimdv 2645 . . . . . 6  |-  ( ( 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 ) ) )
133132ralrimiv 2638 . . . . 5  |-  ( ( 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 ) )
134 frn 5411 . . . . . . . . . . . 12  |-  ( h : om --> S  ->  ran  h  C_  S )
135 ffun 5407 . . . . . . . . . . . . . . . 16  |-  ( s : suc  n --> A  ->  Fun  s )
1361353ad2ant1 976 . . . . . . . . . . . . . . 15  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  Fun  s )
137136rexlimivw 2676 . . . . . . . . . . . . . 14  |-  ( E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  Fun  s )
138137ss2abi 3258 . . . . . . . . . . . . 13  |-  { 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 }
13928, 138eqsstri 3221 . . . . . . . . . . . 12  |-  S  C_  { s  |  Fun  s }
140134, 139syl6ss 3204 . . . . . . . . . . 11  |-  ( h : om --> S  ->  ran  h  C_  { s  |  Fun  s } )
141140sseld 3192 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  u  e.  {
s  |  Fun  s } ) )
142 vex 2804 . . . . . . . . . . 11  |-  u  e. 
_V
143 funeq 5290 . . . . . . . . . . 11  |-  ( s  =  u  ->  ( Fun  s  <->  Fun  u ) )
144142, 143elab 2927 . . . . . . . . . 10  |-  ( u  e.  { s  |  Fun  s }  <->  Fun  u )
145141, 144syl6ib 217 . . . . . . . . 9  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  Fun  u )
)
146145adantr 451 . . . . . . . 8  |-  ( ( h : om --> S  /\  A. m  e.  om  A. j  e.  m  (
h `  j )  C_  ( h `  m
) )  ->  (
u  e.  ran  h  ->  Fun  u ) )
147 ffn 5405 . . . . . . . . 9  |-  ( h : om --> S  ->  h  Fn  om )
148 fvelrnb 5586 . . . . . . . . . . . . 13  |-  ( h  Fn  om  ->  (
v  e.  ran  h  <->  E. b  e.  om  (
h `  b )  =  v ) )
149 fvelrnb 5586 . . . . . . . . . . . . . . 15  |-  ( h  Fn  om  ->  (
u  e.  ran  h  <->  E. a  e.  om  (
h `  a )  =  u ) )
150 nnord 4680 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  e.  om  ->  Ord  a )
151 nnord 4680 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  om  ->  Ord  b )
152150, 151anim12i 549 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  om  /\  b  e.  om )  ->  ( Ord  a  /\  Ord  b ) )
153 ordtri3or 4440 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Ord  a  /\  Ord  b )  ->  (
a  e.  b  \/  a  =  b  \/  b  e.  a ) )
154 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  b  ->  (
h `  m )  =  ( h `  b ) )
155154sseq2d 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  b  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  b )
) )
156155raleqbi1dv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  b  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  b  ( h `  j )  C_  (
h `  b )
) )
157156rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 )
) )
158 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  a  ->  (
h `  j )  =  ( h `  a ) )
159158sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  a  ->  (
( h `  j
)  C_  ( h `  b )  <->  ( h `  a )  C_  (
h `  b )
) )
160159rspccv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  b  (
h `  j )  C_  ( h `  b
)  ->  ( a  e.  b  ->  ( h `
 a )  C_  ( h `  b
) ) )
161157, 160syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( b  e.  om  ->  ( A. m  e.  om  A. j  e.  m  ( h `  j ) 
C_  ( h `  m )  ->  (
a  e.  b  -> 
( h `  a
)  C_  ( h `  b ) ) ) )
162161adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) ) )
1631623imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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
) )
164163orcd 381 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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
) ) )
1651643exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) ) ) ) )
166165com3r 73 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) ) )
167 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  b  ->  (
h `  a )  =  ( h `  b ) )
168 eqimss 3243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  a )  =  ( h `  b )  ->  (
h `  a )  C_  ( h `  b
) )
169168orcd 381 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  a )  =  ( h `  b )  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
170167, 169syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  b  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
171170a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  b  ->  ( A. m  e.  om  A. j  e.  m  ( h `  j ) 
C_  ( h `  m )  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) ) )
172171a1d 22 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) ) )
173 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  a  ->  (
h `  m )  =  ( h `  a ) )
174173sseq2d 3219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  a  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  a )
) )
175174raleqbi1dv 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  a  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  a  ( h `  j )  C_  (
h `  a )
) )
176175rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 )
) )
177 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  b  ->  (
h `  j )  =  ( h `  b ) )
178177sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  b  ->  (
( h `  j
)  C_  ( h `  a )  <->  ( h `  b )  C_  (
h `  a )
) )
179178rspccv 2894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  a  (
h `  j )  C_  ( h `  a
)  ->  ( b  e.  a  ->  ( h `
 b )  C_  ( h `  a
) ) )
180176, 179syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( a  e.  om  ->  ( A. m  e.  om  A. j  e.  m  ( h `  j ) 
C_  ( h `  m )  ->  (
b  e.  a  -> 
( h `  b
)  C_  ( h `  a ) ) ) )
181180adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) ) )
1821813imp 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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
) )
183182olcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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
) ) )
1841833exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) ) ) ) )
185184com3r 73 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) ) )
186166, 172, 1853jaoi 1245 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 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
) ) ) ) )
187153, 186syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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
) ) ) ) )
188152, 187mpcom 32 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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
) ) ) )
189 sseq12 3214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 a )  C_  ( h `  b
)  <->  u  C_  v ) )
190 sseq12 3214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h `  b
)  =  v  /\  ( h `  a
)  =  u )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
191190ancoms 439 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
192189, 191orbi12d 690 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( ( h `  a ) 
C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  <->  ( u  C_  v  \/  v  C_  u ) ) )
193192biimpcd 215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  ->  (
( ( h `  a )  =  u  /\  ( h `  b )  =  v )  ->  ( u  C_  v  \/  v  C_  u ) ) )
194188, 193syl6 29 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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 ) ) ) )
195194com23 72 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 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 ) ) ) )
196195exp4b 590 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) ) ) ) ) )
197196com23 72 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) ) )
198197rexlimiv 2674 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) ) )
199198rexlimdv 2679 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
200149, 199syl6bi 219 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) ) )
201200com23 72 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) ) )
202148, 201sylbid 206 . . . . . . . . . . . 12  |-  ( 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 ) ) ) ) )
203202com24 81 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
204203imp 418 . . . . . . . . . 10  |-  ( ( 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 ) ) ) )
205204ralrimdv 2645 . . . . . . . . 9  |-  ( ( 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 ) ) )
206147, 205sylan 457 . . . . . . . 8  |-  ( ( 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 ) ) )
207146, 206jcad 519 . . . . . . 7  |-  ( ( 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 ) ) ) )
208207ralrimiv 2638 . . . . . 6  |-  ( ( 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 ) ) )
209 fununi 5332 . . . . . 6  |-  ( A. u  e.  ran  h ( Fun  u  /\  A. v  e.  ran  h ( u  C_  v  \/  v  C_  u ) )  ->  Fun  U. ran  h
)
210208, 209syl 15 . . . . 5  |-  ( ( h : om --> S  /\  A. m  e.  om  A. j  e.  m  (
h `  j )  C_  ( h `  m
) )  ->  Fun  U.
ran  h )
211133, 210syldan 456 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  Fun  U. ran  h )
212 vex 2804 . . . . . . . . 9  |-  m  e. 
_V
213212eldm2 4893 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u <. m ,  u >.  e.  U. ran  h )
214 eluni2 3847 . . . . . . . . . 10  |-  ( <.
m ,  u >.  e. 
U. ran  h  <->  E. v  e.  ran  h <. m ,  u >.  e.  v
)
215212, 142opeldm 4898 . . . . . . . . . . . . . . 15  |-  ( <.
m ,  u >.  e.  v  ->  m  e.  dom  v )
216215a1i 10 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  v  ->  m  e.  dom  v ) )
217134, 44syl6ss 3204 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) } )
218 ssel 3187 . . . . . . . . . . . . . . . 16  |-  ( 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 ) } ) )
219 vex 2804 . . . . . . . . . . . . . . . . . 18  |-  v  e. 
_V
220 dmeq 4895 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  v  ->  dom  s  =  dom  v )
221220eleq2d 2363 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  v ) )
222220eleq1d 2362 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( dom  s  e.  om  <->  dom  v  e.  om )
)
223221, 222anbi12d 691 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  v  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) ) )
224219, 223elab 2927 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) )
225224simprbi 450 . . . . . . . . . . . . . . . 16  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  dom  v  e.  om )
226218, 225syl6 29 . . . . . . . . . . . . . . 15  |-  ( ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  ( v  e.  ran  h  ->  dom  v  e.  om ) )
227217, 226syl 15 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  dom  v  e.  om ) )
228216, 227anim12d 546 . . . . . . . . . . . . 13  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  (
m  e.  dom  v  /\  dom  v  e.  om ) ) )
229 elnn 4682 . . . . . . . . . . . . 13  |-  ( ( m  e.  dom  v  /\  dom  v  e.  om )  ->  m  e.  om )
230228, 229syl6 29 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  m  e.  om ) )
231230exp3acom23 1362 . . . . . . . . . . 11  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  ( <. m ,  u >.  e.  v  ->  m  e.  om )
) )
232231rexlimdv 2679 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( E. v  e. 
ran  h <. m ,  u >.  e.  v  ->  m  e.  om )
)
233214, 232syl5bi 208 . . . . . . . . 9  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  U. ran  h  ->  m  e.  om )
)
234233exlimdv 1626 . . . . . . . 8  |-  ( h : om --> S  -> 
( E. u <. m ,  u >.  e.  U. ran  h  ->  m  e.  om ) )
235213, 234syl5bi 208 . . . . . . 7  |-  ( h : om --> S  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
236235adantr 451 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
237129simpld 445 . . . . . . . . 9  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  m  e.  dom  ( h `  m ) )
238 fnfvelrn 5678 . . . . . . . . . . . . 13  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( h `  m
)  e.  ran  h
)
239 dmeq 4895 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( h `  m )  ->  dom  u  =  dom  ( h `
 m ) )
240239eleq2d 2363 . . . . . . . . . . . . . . 15  |-  ( u  =  ( h `  m )  ->  (
m  e.  dom  u  <->  m  e.  dom  ( h `
 m ) ) )
241240rspcev 2897 . . . . . . . . . . . . . 14  |-  ( ( ( h `  m
)  e.  ran  h  /\  m  e.  dom  ( h `  m
) )  ->  E. u  e.  ran  h  m  e. 
dom  u )
242241ex 423 . . . . . . . . . . . . 13  |-  ( ( h `  m )  e.  ran  h  -> 
( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
243238, 242syl 15 . . . . . . . . . . . 12  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
244147, 243sylan 457 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
245244ancoms 439 . . . . . . . . . 10  |-  ( ( m  e.  om  /\  h : om --> S )  ->  ( m  e. 
dom  ( h `  m )  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
246245adantrr 697 . . . . . . . . 9  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
m  e.  dom  (
h `  m )  ->  E. u  e.  ran  h  m  e.  dom  u ) )
247237, 246mpd 14 . . . . . . . 8  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  E. u  e.  ran  h  m  e. 
dom  u )
248 dmuni 4904 . . . . . . . . . 10  |-  dom  U. ran  h  =  U_ u  e.  ran  h dom  u
249248eleq2i 2360 . . . . . . . . 9  |-  ( m  e.  dom  U. ran  h 
<->  m  e.  U_ u  e.  ran  h dom  u
)
250 eliun 3925 . . . . . . . . 9  |-  ( m  e.  U_ u  e. 
ran  h dom  u  <->  E. u  e.  ran  h  m  e.  dom  u )
251249, 250bitri 240 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u  e.  ran  h  m  e.  dom  u )
252247, 251sylibr 203 . . . . . . 7  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  m  e.  dom  U. ran  h
)
253252expcom 424 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  U. ran  h ) )
254236, 253impbid 183 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  dom  U.
ran  h  <->  m  e.  om ) )
255254eqrdv 2294 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  dom  U. ran  h  =  om )
256 rnuni 5108 . . . . . 6  |-  ran  U. ran  h  =  U_ s  e.  ran  h ran  s
257 frn 5411 . . . . . . . . . . . . . 14  |-  ( s : suc  n --> A  ->  ran  s  C_  A )
2582573ad2ant1 976 . . . . . . . . . . . . 13  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ran  s  C_  A )
259258rexlimivw 2676 . . . . . . . . . . . 12  |-  ( 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 )
260259ss2abi 3258 . . . . . . . . . . 11  |-  { 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 }
26128, 260eqsstri 3221 . . . . . . . . . 10  |-  S  C_  { s  |  ran  s  C_  A }
262134, 261syl6ss 3204 . . . . . . . . 9  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ran  s  C_  A } )
263 ssel 3187 . . . . . . . . . 10  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  s  e.  { s  |  ran  s  C_  A } ) )
264 abid 2284 . . . . . . . . . 10  |-  ( s  e.  { s  |  ran  s  C_  A } 
<->  ran  s  C_  A
)
265263, 264syl6ib 217 . . . . . . . . 9  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  ran  s  C_  A ) )
266262, 265syl 15 . . . . . . . 8  |-  ( h : om --> S  -> 
( s  e.  ran  h  ->  ran  s  C_  A ) )
267266ralrimiv 2638 . . . . . . 7  |-  ( h : om --> S  ->  A. s  e.  ran  h ran  s  C_  A
)
268 iunss 3959 . . . . . . 7  |-  ( U_ s  e.  ran  h ran  s  C_  A  <->  A. s  e.  ran  h ran  s  C_  A )
269267, 268sylibr 203 . . . . . 6  |-  ( h : om --> S  ->  U_ s  e.  ran  h ran  s  C_  A
)
270256, 269syl5eqss 3235 . . . . 5  |-  ( h : om --> S  ->  ran  U. ran  h  C_  A )
271270adantr 451 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  ran  U. ran  h  C_  A )
272 df-fn 5274 . . . . 5  |-  ( U. ran  h  Fn  om  <->  ( Fun  U.
ran  h  /\  dom  U.
ran  h  =  om ) )
273 df-f 5275 . . . . . 6  |-  ( U. ran  h : om --> A  <->  ( U. ran  h  Fn  om  /\  ran  U. ran  h  C_  A ) )
274273biimpri 197 . . . . 5  |-  ( ( U. ran  h  Fn 
om  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
275272, 274sylanbr 459 . . . 4  |-  ( ( ( Fun  U. ran  h  /\  dom  U. ran  h  =  om )  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
276211, 255, 271, 275syl21anc 1181 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  U. ran  h : om --> A )
277 fnfvelrn 5678 . . . . . . . 8  |-  ( ( h  Fn  om  /\  (/) 
e.  om )  ->  (
h `  (/) )  e. 
ran  h )
278147, 25, 277sylancl 643 . . . . . . 7  |-  ( h : om --> S  -> 
( h `  (/) )  e. 
ran  h )
279278adantr 451 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  e. 
ran  h )
280 elssuni 3871 . . . . . 6  |-  ( ( h `  (/) )  e. 
ran  h  ->  (
h `  (/) )  C_  U.
ran  h )
281279, 280syl 15 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  C_  U.
ran  h )
28254adantr 451 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  (/) 
e.  dom  ( h `  (/) ) )
283 funssfv 5559 . . . . 5  |-  ( ( Fun  U. ran  h  /\  ( h `  (/) )  C_  U.
ran  h  /\  (/)  e.  dom  ( h `  (/) ) )  ->  ( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
284211, 281, 282, 283syl3anc 1182 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
285 simp2 956 . . . . . . . . . . 11  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
286285rexlimivw 2676 . . . . . . . . . 10  |-  ( E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
287286ss2abi 3258 . . . . . . . . 9  |-  { 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 }
28828, 287eqsstri 3221 . . . . . . . 8  |-  S  C_  { s  |  ( s `
 (/) )  =  C }
289134, 288syl6ss 3204 . . . . . . 7  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( s `  (/) )  =  C }
)
290 ssel 3187 . . . . . . . 8  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C } ) )
291 fveq1 5540 . . . . . . . . . 10  |-  ( s  =  ( h `  (/) )  ->  ( s `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
292291eqeq1d 2304 . . . . . . . . 9  |-  ( s  =  ( h `  (/) )  ->  ( (
s `  (/) )  =  C  <->  ( ( h `
 (/) ) `  (/) )  =  C ) )
29346, 292elab 2927 . . . . . . . 8  |-  ( ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C }  <->  ( (
h `  (/) ) `  (/) )  =  C )
294290, 293syl6ib 217 . . . . . . 7  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
295289, 294syl 15 . . . . . 6  |-  ( h : om --> S  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
296295adantr 451 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
297279, 296mpd 14 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) ) `  (/) )  =  C )
298284, 297eqtrd 2328 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  C )
299 nfv 1609 . . . . 5  |-  F/ k  h : om --> S
300 nfra1 2606 . . . . 5  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
301299, 300nfan 1783 . . . 4  |-  F/ k ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
302134ad2antrr 706 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ran  h  C_  S )
303 peano2 4692 . . . . . . . . 9  |-  ( k  e.  om  ->  suc  k  e.  om )
304 fnfvelrn 5678 . . . . . . . . 9  |-  ( ( h  Fn  om  /\  suc  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
305147, 303, 304syl2an 463 . . . . . . . 8  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
306305adantlr 695 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ran  h )
307237expcom 424 . . . . . . . . 9  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  (
h `  m )
) )
308307ralrimiv 2638 . . . . . . . 8  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  A. m  e.  om  m  e.  dom  ( h `
 m ) )
309 id 19 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  m  =  suc  k )
310 fveq2 5541 . . . . . . . . . . . 12  |-  ( m  =  suc  k  -> 
( h `  m
)  =  ( h `
 suc  k )
)
311310dmeqd 4897 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  dom  ( h `  m
)  =  dom  (
h `  suc  k ) )
312309, 311eleq12d 2364 . . . . . . . . . 10  |-  ( m  =  suc  k  -> 
( m  e.  dom  ( h `  m
)  <->  suc  k  e.  dom  ( h `  suc  k ) ) )
313312rspcv 2893 . . . . . . . . 9  |-  ( suc  k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
314303, 313syl 15 . . . . . . . 8  |-  ( k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
315308, 314mpan9 455 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  suc  k  e.  dom  ( h `
 suc  k )
)
316 eleq2 2357 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom  s  =  suc  n  ->  ( suc  k  e. 
dom  s  <->  suc  k  e. 
suc  n ) )
317316biimpa 470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( dom  s  =  suc  n  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
31829, 317sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s : suc  n --> A  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
319 ordsucelsuc 4629 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord  n  ->  ( k  e.  n  <->  suc  k  e.  suc  n ) )
32030, 319syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  om  ->  (
k  e.  n  <->  suc  k  e. 
suc  n ) )
321320biimprd 214 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  om  ->  ( suc  k  e.  suc  n  ->  k  e.  n
) )
322 rsp 2616 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. k  e.  n  (
s `  suc  k )  e.  ( F `  ( s `  k
) )  ->  (
k  e.  n  -> 
( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) )
323321, 322syl9r 67 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 ) ) ) ) )
324323com13 74 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) ) ) )
325318, 324syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) ) )
326325ex 423 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) ) )
327326com24 81 . . . . . . . . . . . . . . . 16  |-  ( 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
) ) ) ) ) )
328327imp 418 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) ) )
3293283adant2 974 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) ) ) )
330329impcom 419 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) ) )
331330rexlimiva 2675 . . . . . . . . . . . 12  |-  ( 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
) ) ) )
332331ss2abi 3258 . . . . . . . . . . 11  |-  { 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 ) ) ) }
33328, 332eqsstri 3221 . . . . . . . . . 10  |-  S  C_  { s  |  ( suc  k  e.  dom  s  ->  ( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) }
334 sstr 3200 . . . . . . . . . 10  |-  ( ( 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 ) ) ) } )
335333, 334mpan2 652 . . . . . . . . 9  |-  ( ran  h  C_  S  ->  ran  h  C_  { s  |  ( suc  k  e.  dom  s  ->  (
s `  suc  k )  e.  ( F `  ( s `  k
) ) ) } )
336335sseld 3192 . . . . . . . 8  |-  ( 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 ) ) ) } ) )
337 fvex 5555 . . . . . . . . 9  |-  ( h `
 suc  k )  e.  _V
338 dmeq 4895 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  dom  s  =  dom  ( h `
 suc  k )
)
339338eleq2d 2363 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  ( suc  k  e.  dom  s 
<->  suc  k  e.  dom  ( h `  suc  k ) ) )
340 fveq1 5540 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  (
s `  suc  k )  =  ( ( h `
 suc  k ) `  suc  k ) )
341 fveq1 5540 . . . . . . . . . . . 12  |-  ( s  =  ( h `  suc  k )  ->  (
s `  k )  =  ( ( h `
 suc  k ) `  k ) )
342341fveq2d 5545 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  ( F `  ( s `  k ) )  =  ( F `  (
( h `  suc  k ) `  k
) ) )
343340, 342eleq12d 2364 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  (
( s `  suc  k )  e.  ( F `  ( s `
 k ) )  <-> 
( ( h `  suc  k ) `  suc  k )  e.  ( F `  ( ( h `  suc  k
) `  k )
) ) )
344339, 343imbi12d 311 . . . . . . . . 9  |-  ( 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 )
) ) ) )
345337, 344elab 2927 . . . . . . . 8  |-  ( ( 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 )
) ) )
346336, 345syl6ib 217 . . . . . . 7  |-  ( 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 )
) ) ) )
347302, 306, 315, 346syl3c 57 . . . . . 6  |-  ( ( ( 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 )
) )
348211adantr 451 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  Fun  U.
ran  h )
349 elssuni 3871 . . . . . . . . . 10  |-  ( ( h `  suc  k
)  e.  ran  h  ->  ( h `  suc  k )  C_  U. ran  h )
350305, 349syl 15 . . . . . . . . 9  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  C_  U. ran  h )
351350adantlr 695 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k ) 
C_  U. ran  h )
352 funssfv 5559 . . . . . . . 8  |-  ( ( 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 ) )
353348, 351, 315, 352syl3anc 1182 . . . . . . 7  |-  ( ( ( 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 ) )
354217sseld 3192 . . . . . . . . . . . . . . . 16  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( h `  suc  k )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } ) )
355338eleq2d 2363 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  suc  k )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  suc  k ) ) )
356338eleq1d 2362 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  suc  k )  ->  ( dom  s  e.  om  <->  dom  ( h `  suc  k )  e.  om ) )
357355, 356anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
358337, 357elab 2927 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  k
)  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
359354, 358syl6ib 217 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
360359adantr 451 . . . . . . . . . . . . . 14  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
361305, 360mpd 14 . . . . . . . . . . . . 13  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
362361simprd 449 . . . . . . . . . . . 12  |-  ( ( h : om --> S  /\  k  e.  om )  ->  dom  ( h `  suc  k )  e.  om )
363 nnord 4680 . . . . . . . . . . . 12  |-  ( dom  ( h `  suc  k )  e.  om  ->  Ord  dom  ( h `  suc  k ) )
364362, 363syl 15 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  k  e.  om )  ->  Ord  dom  ( h `  suc  k ) )
365 ordtr 4422 . . . . . . . . . . 11  |-  ( Ord 
dom  ( h `  suc  k )  ->  Tr  dom  ( h `  suc  k ) )
366 trsuc 4492 . . . . . . . . . . . 12  |-  ( ( Tr  dom  ( h `
 suc  k )  /\  suc  k  e.  dom  ( h `  suc  k ) )  -> 
k  e.  dom  (
h `  suc  k ) )
367366ex 423 . . . . . . . . . . 11  |-  ( Tr 
dom  ( h `  suc  k )  ->  ( suc  k  e.  dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
368364, 365, 3673syl 18 . . . . . . . . . 10  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( suc  k  e. 
dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
369368adantlr 695 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
370315, 369mpd 14 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  k  e.  dom  ( h `  suc  k ) )
371 funssfv 5559 . . . . . . . 8  |-  ( ( 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
) )
372348, 351, 370, 371syl3anc 1182 . . . . . . 7  |-  ( ( ( 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 )
)
373 simpl 443 . . . . . . . 8  |-  ( ( ( 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 ) )
374 simpr 447 . . . . . . . . 9  |-  ( ( ( 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 ) )
375374fveq2d 5545 . . . . . . . 8  |-  ( ( ( 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
) ) )
376373, 375eleq12d 2364 . . . . . . 7  |-  ( ( ( 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
) ) ) )
377353, 372, 376syl2anc 642 . . . . . 6  |-  ( ( ( 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
) ) ) )
378347, 377mpbird 223 . . . . 5  |-  ( ( ( 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 ) ) )
379378ex 423 . . . 4  |-  ( ( 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
) ) ) )
380301, 379ralrimi 2637 . . 3  |-  ( ( 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 ) ) )
381 vex 2804 . . . . . 6  |-  h  e. 
_V
382381rnex 4958 . . . . 5  |-  ran  h  e.  _V
383382uniex 4532 . . . 4  |-  U. ran  h  e.  _V
384 feq1 5391 . . . . 5  |-  ( g  =  U. ran  h  ->  ( g : om --> A 
<-> 
U. ran  h : om
--> A ) )
385 fveq1 5540 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( g `  (/) )  =  ( U. ran  h `  (/) ) )
386385eqeq1d 2304 . . . . 5  |-  ( g  =  U. ran  h  ->  ( ( g `  (/) )  =  C  <->  ( U. ran  h `  (/) )  =  C ) )
387 fveq1 5540 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( g `  suc  k )  =  ( U. ran  h `  suc  k ) )
388 fveq1 5540 . . . . . . . 8  |-  ( g  =  U. ran  h  ->  ( g `  k
)  =  ( U. ran  h `  k ) )
389388fveq2d 5545 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( F `  (
g `  k )
)  =  ( F `
 ( U. ran  h `  k )
) )
390387, 389eleq12d 2364 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) ) ) )
391390ralbidv 2576 . . . . 5  |-  ( 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 ) ) ) )
392384, 386, 3913anbi123d 1252 . . . 4  |-  ( 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 ) ) ) ) )
393383, 392spcev 2888 . . 3  |-  ( ( 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 ) ) ) )
394276, 298, 380, 393syl3anc 1182 . 2  |-  ( ( 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 ) ) ) )
395394exlimiv 1624 1  |-  ( 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 ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    /\ w3a 934   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    C_ wss 3165   (/)c0 3468   <.cop 3656   U.cuni 3843   U_ciun 3921    e. cmpt 4093   Tr wtr 4129   Ord word 4407   suc csuc 4410   omcom 4672   dom cdm 4705   ran crn 4706    |` cres 4707   Fun wfun 5265    Fn wfn 5266   -->wf 5267   ` cfv 5271
This theorem is referenced by:  axdc3lem4  8095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-dc 8088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279  df-1o 6495
  Copyright terms: Public domain W3C validator