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

Theorem axdc3lem2 8879
Description: Lemma for axdc3 8882. 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 8874 (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 8874 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 23 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  m  =  (/) )
2 fveq2 5881 . . . . . . . . . . . . . 14  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
32dmeqd 5057 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  dom  (
h `  m )  =  dom  ( h `  (/) ) )
41, 3eleq12d 2511 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( m  e.  dom  ( h `
 m )  <->  (/)  e.  dom  ( h `  (/) ) ) )
5 eleq2 2502 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( j  e.  m  <->  j  e.  (/) ) )
62sseq2d 3498 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( ( h `  j ) 
C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  (/) ) ) )
75, 6imbi12d 321 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( ( j  e.  m  -> 
( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) ) ) )
84, 7anbi12d 715 . . . . . . . . . . 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 23 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  m  =  i )
10 fveq2 5881 . . . . . . . . . . . . . 14  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
1110dmeqd 5057 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  dom  ( h `  m
)  =  dom  (
h `  i )
)
129, 11eleq12d 2511 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
m  e.  dom  (
h `  m )  <->  i  e.  dom  ( h `
 i ) ) )
13 elequ2 1875 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
j  e.  m  <->  j  e.  i ) )
1410sseq2d 3498 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  i )
) )
1513, 14imbi12d 321 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
( j  e.  m  ->  ( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  i  ->  ( h `
 j )  C_  ( h `  i
) ) ) )
1612, 15anbi12d 715 . . . . . . . . . . 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 23 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  m  =  suc  i )
18 fveq2 5881 . . . . . . . . . . . . . 14  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
1918dmeqd 5057 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  dom  ( h `  m
)  =  dom  (
h `  suc  i ) )
2017, 19eleq12d 2511 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( m  e.  dom  ( h `  m
)  <->  suc  i  e.  dom  ( h `  suc  i ) ) )
21 eleq2 2502 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( j  e.  m  <->  j  e.  suc  i ) )
2218sseq2d 3498 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( ( h `  j )  C_  (
h `  m )  <->  ( h `  j ) 
C_  ( h `  suc  i ) ) )
2321, 22imbi12d 321 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( ( j  e.  m  ->  ( h `  j )  C_  (
h `  m )
)  <->  ( j  e. 
suc  i  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
2420, 23anbi12d 715 . . . . . . . . . . 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 6726 . . . . . . . . . . . . . . 15  |-  (/)  e.  om
26 ffvelrn 6035 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  (/) 
e.  om )  ->  (
h `  (/) )  e.  S )
2725, 26mpan2 675 . . . . . . . . . . . . . 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 5750 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s : suc  n --> A  ->  dom  s  =  suc  n )
30 nnord 6714 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  om  ->  Ord  n )
31 0elsuc 6676 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord  n  ->  (/)  e.  suc  n )
3230, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  (/)  e.  suc  n )
33 peano2 6727 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  suc  n  e.  om )
34 eleq2 2502 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s 
<->  (/)  e.  suc  n ) )
35 eleq1 2501 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( dom  s  e. 
om 
<->  suc  n  e.  om ) )
3634, 35anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  s  =  suc  n  ->  ( ( (/)  e.  dom  s  /\  dom  s  e. 
om )  <->  ( (/)  e.  suc  n  /\  suc  n  e. 
om ) ) )
3736biimprcd 228 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
(/)  e.  suc  n  /\  suc  n  e.  om )  ->  ( dom  s  =  suc  n  ->  ( (/) 
e.  dom  s  /\  dom  s  e.  om ) ) )
3832, 33, 37syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  om  ->  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
3929, 38syl5com 31 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s : suc  n --> A  -> 
( n  e.  om  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
40393ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . . . . . . . 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 2920 . . . . . . . . . . . . . . . . . . 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 3539 . . . . . . . . . . . . . . . . . 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 3500 . . . . . . . . . . . . . . . . 17  |-  S  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) }
4544sseli 3466 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e.  S  ->  ( h `  (/) )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } )
46 fvex 5891 . . . . . . . . . . . . . . . . 17  |-  ( h `
 (/) )  e.  _V
47 dmeq 5055 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  ( h `  (/) )  ->  dom  s  =  dom  ( h `  (/) ) )
4847eleq2d 2499 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( (/)  e.  dom  s 
<->  (/)  e.  dom  ( h `
 (/) ) ) )
4947eleq1d 2498 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( dom  s  e.  om  <->  dom  ( h `
 (/) )  e.  om ) )
5048, 49anbi12d 715 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  (/) )  ->  ( ( (/) 
e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) ) )
5146, 50elab 3224 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e. 
{ s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) }  <->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5245, 51sylib 199 . . . . . . . . . . . . . . 15  |-  ( ( h `  (/) )  e.  S  ->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5352simpld 460 . . . . . . . . . . . . . 14  |-  ( ( h `  (/) )  e.  S  ->  (/)  e.  dom  ( h `  (/) ) )
5427, 53syl 17 . . . . . . . . . . . . 13  |-  ( h : om --> S  ->  (/) 
e.  dom  ( h `  (/) ) )
55 noel 3771 . . . . . . . . . . . . . 14  |-  -.  j  e.  (/)
5655pm2.21i 134 . . . . . . . . . . . . 13  |-  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) )
5754, 56jctir 540 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) )
5857adantr 466 . . . . . . . . . . 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 6035 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  i  e.  om )  ->  ( h `  i
)  e.  S )
6059ancoms 454 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  h : om --> S )  ->  ( h `  i )  e.  S
)
6160adantrr 721 . . . . . . . . . . . . 13  |-  ( ( i  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
h `  i )  e.  S )
62 suceq 5507 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  suc  k  =  suc  i )
6362fveq2d 5885 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
64 fveq2 5881 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
6564fveq2d 5885 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
6663, 65eleq12d 2511 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
6766rspcva 3186 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )
6867adantrl 720 . . . . . . . . . . . . 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 3466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  S  ->  (
h `  i )  e.  { s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) } )
70 fvex 5891 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h `
 i )  e. 
_V
71 dmeq 5055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( h `  i )  ->  dom  s  =  dom  ( h `
 i ) )
7271eleq2d 2499 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  i
) ) )
7371eleq1d 2498 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( dom  s  e.  om  <->  dom  ( h `  i
)  e.  om )
)
7472, 73anbi12d 715 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( h `  i )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) ) )
7570, 74elab 3224 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) )
7669, 75sylib 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  i )  e.  S  ->  ( (/) 
e.  dom  ( h `  i )  /\  dom  ( h `  i
)  e.  om )
)
7776simprd 464 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  i )  e.  S  ->  dom  ( h `  i
)  e.  om )
78 nnord 6714 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( h `  i
)  e.  om  ->  Ord 
dom  ( h `  i ) )
79 ordsucelsuc 6663 . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . 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 5055 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( h `  i )  ->  dom  x  =  dom  ( h `
 i ) )
83 suceq 5507 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  x  =  dom  (
h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i ) )
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i
) )
8584eqeq2d 2443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  ( dom  y  =  suc  dom  x  <->  dom  y  =  suc  dom  ( h `  i
) ) )
8682reseq2d 5125 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  (
y  |`  dom  x )  =  ( y  |`  dom  ( h `  i
) ) )
87 id 23 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  x  =  ( h `  i ) )
8886, 87eqeq12d 2451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  (
( y  |`  dom  x
)  =  x  <->  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) )
8985, 88anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . 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 3079 . . . . . . . . . . . . . . . . . . . . . 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 8878 . . . . . . . . . . . . . . . . . . . . . . 23  |-  S  e. 
_V
9493rabex 4576 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i
)  /\  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) }  e.  _V
9590, 91, 94fvmpt 5964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  i )  e.  S  ->  ( G `  ( h `  i ) )  =  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i )  /\  (
y  |`  dom  ( h `
 i ) )  =  ( h `  i ) ) } )
9695eleq2d 2499 . . . . . . . . . . . . . . . . . . . 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 5055 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  dom  y  =  dom  ( h `
 suc  i )
)
9897eqeq1d 2431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  ( dom  y  =  suc  dom  ( h `  i
)  <->  dom  ( h `  suc  i )  =  suc  dom  ( h `  i
) ) )
99 reseq1 5119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  (
y  |`  dom  ( h `
 i ) )  =  ( ( h `
 suc  i )  |` 
dom  ( h `  i ) ) )
10099eqeq1d 2431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  (
( y  |`  dom  (
h `  i )
)  =  ( h `
 i )  <->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) ) )
10198, 100anbi12d 715 . . . . . . . . . . . . . . . . . . . . 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 3235 . . . . . . . . . . . . . . . . . . . 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 264 . . . . . . . . . . . . . . . . . . 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 628 . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  dom  ( h `
 suc  i )  =  suc  dom  ( h `  i ) )
106105eleq2d 2499 . . . . . . . . . . . . . . . 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 259 . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) )
110 resss 5148 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  i
)  |`  dom  ( h `
 i ) ) 
C_  ( h `  suc  i )
111 sseq1 3491 . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  suc  i )  |`  dom  (
h `  i )
)  =  ( h `
 i )  -> 
( h `  i
)  C_  ( h `  suc  i ) )
113 elsuci 5508 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  suc  i  -> 
( j  e.  i  \/  j  =  i ) )
114 pm2.27 40 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( h `  j )  C_  (
h `  i )
) )
115 sstr2 3477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  j ) 
C_  ( h `  i )  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
116114, 115syl6 34 . . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  (
h `  j )  =  ( h `  i ) )
118117sseq1d 3497 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
( h `  j
)  C_  ( h `  suc  i )  <->  ( h `  i )  C_  (
h `  suc  i ) ) )
119118biimprd 226 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
120119a1d 26 . . . . . . . . . . . . . . . . . 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 380 . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . 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 83 . . . . . . . . . . . . . . 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 565 . . . . . . . . . . . . 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 665 . . . . . . . . . . . 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 435 . . . . . . . . . . 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 6735 . . . . . . . . . 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 430 . . . . . . . . 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 464 . . . . . . . 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 436 . . . . . . 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 2848 . . . . . 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 2844 . . . . 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 5752 . . . . . . . . . . . 12  |-  ( h : om --> S  ->  ran  h  C_  S )
135 ffun 5748 . . . . . . . . . . . . . . . 16  |-  ( s : suc  n --> A  ->  Fun  s )
1361353ad2ant1 1026 . . . . . . . . . . . . . . 15  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  Fun  s )
137136rexlimivw 2921 . . . . . . . . . . . . . 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 3539 . . . . . . . . . . . . 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 3500 . . . . . . . . . . . 12  |-  S  C_  { s  |  Fun  s }
140134, 139syl6ss 3482 . . . . . . . . . . 11  |-  ( h : om --> S  ->  ran  h  C_  { s  |  Fun  s } )
141140sseld 3469 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  u  e.  {
s  |  Fun  s } ) )
142 vex 3090 . . . . . . . . . . 11  |-  u  e. 
_V
143 funeq 5620 . . . . . . . . . . 11  |-  ( s  =  u  ->  ( Fun  s  <->  Fun  u ) )
144142, 143elab 3224 . . . . . . . . . 10  |-  ( u  e.  { s  |  Fun  s }  <->  Fun  u )
145141, 144syl6ib 229 . . . . . . . . 9  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  Fun  u )
)
146145adantr 466 . . . . . . . 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 5746 . . . . . . . . 9  |-  ( h : om --> S  ->  h  Fn  om )
148 fvelrnb 5928 . . . . . . . . . . . . 13  |-  ( h  Fn  om  ->  (
v  e.  ran  h  <->  E. b  e.  om  (
h `  b )  =  v ) )
149 fvelrnb 5928 . . . . . . . . . . . . . . 15  |-  ( h  Fn  om  ->  (
u  e.  ran  h  <->  E. a  e.  om  (
h `  a )  =  u ) )
150 nnord 6714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  e.  om  ->  Ord  a )
151 nnord 6714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  om  ->  Ord  b )
152150, 151anim12i 568 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  om  /\  b  e.  om )  ->  ( Ord  a  /\  Ord  b ) )
153 ordtri3or 5474 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Ord  a  /\  Ord  b )  ->  (
a  e.  b  \/  a  =  b  \/  b  e.  a ) )
154 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  b  ->  (
h `  m )  =  ( h `  b ) )
155154sseq2d 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  b  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  b )
) )
156155raleqbi1dv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  b  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  b  ( h `  j )  C_  (
h `  b )
) )
157156rspcv 3184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  a  ->  (
h `  j )  =  ( h `  a ) )
159158sseq1d 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  a  ->  (
( h `  j
)  C_  ( h `  b )  <->  ( h `  a )  C_  (
h `  b )
) )
160159rspccv 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  b  (
h `  j )  C_  ( h `  b
)  ->  ( a  e.  b  ->  ( h `
 a )  C_  ( h `  b
) ) )
161157, 160syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 393 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . . . . . 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 82 . . . . . . . . . . . . . . . . . . . . . . . 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 5881 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  b  ->  (
h `  a )  =  ( h `  b ) )
168 eqimss 3522 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  a )  =  ( h `  b )  ->  (
h `  a )  C_  ( h `  b
) )
169168orcd 393 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( h `  a )  =  ( h `  b )  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
170167, 169syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  b  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
1711702a1d 27 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
172 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  a  ->  (
h `  m )  =  ( h `  a ) )
173172sseq2d 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  a  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  a )
) )
174173raleqbi1dv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  a  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  a  ( h `  j )  C_  (
h `  a )
) )
175174rspcv 3184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
176 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  b  ->  (
h `  j )  =  ( h `  b ) )
177176sseq1d 3497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  b  ->  (
( h `  j
)  C_  ( h `  a )  <->  ( h `  b )  C_  (
h `  a )
) )
178177rspccv 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  a  (
h `  j )  C_  ( h `  a
)  ->  ( b  e.  a  ->  ( h `
 b )  C_  ( h `  a
) ) )
179175, 178syl6 34 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
180179adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
1811803imp 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
182181olcd 394 . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
1831823exp 1204 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
184183com3r 82 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
185166, 171, 1843jaoi 1327 . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
186153, 185syl 17 . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
187152, 186mpcom 37 . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
188 sseq12 3493 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 a )  C_  ( h `  b
)  <->  u  C_  v ) )
189 sseq12 3493 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h `  b
)  =  v  /\  ( h `  a
)  =  u )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
190189ancoms 454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
191188, 190orbi12d 714 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( ( h `  a ) 
C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  <->  ( u  C_  v  \/  v  C_  u ) ) )
192191biimpcd 227 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  ->  (
( ( h `  a )  =  u  /\  ( h `  b )  =  v )  ->  ( u  C_  v  \/  v  C_  u ) ) )
193187, 192syl6 34 . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
194193com23 81 . . . . . . . . . . . . . . . . . . 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 ) ) ) )
195194exp4b 610 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
196195com23 81 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
197196rexlimiv 2918 . . . . . . . . . . . . . . . 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 ) ) ) ) )
198197rexlimdv 2922 . . . . . . . . . . . . . . 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 ) ) ) )
199149, 198syl6bi 231 . . . . . . . . . . . . . 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 ) ) ) ) )
200199com23 81 . . . . . . . . . . . . 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 ) ) ) ) )
201148, 200sylbid 218 . . . . . . . . . . . 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 ) ) ) ) )
202201com24 90 . . . . . . . . . . 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 ) ) ) ) )
203202imp 430 . . . . . . . . . 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 ) ) ) )
204203ralrimdv 2848 . . . . . . . . 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 ) ) )
205147, 204sylan 473 . . . . . . . 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 ) ) )
206146, 205jcad 535 . . . . . . 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 ) ) ) )
207206ralrimiv 2844 . . . . . 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 ) ) )
208 fununi 5667 . . . . . 6  |-  ( A. u  e.  ran  h ( Fun  u  /\  A. v  e.  ran  h ( u  C_  v  \/  v  C_  u ) )  ->  Fun  U. ran  h
)
209207, 208syl 17 . . . . 5  |-  ( ( h : om --> S  /\  A. m  e.  om  A. j  e.  m  (
h `  j )  C_  ( h `  m
) )  ->  Fun  U.
ran  h )
210133, 209syldan 472 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  Fun  U. ran  h )
211 vex 3090 . . . . . . . . 9  |-  m  e. 
_V
212211eldm2 5053 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u <. m ,  u >.  e.  U. ran  h )
213 eluni2 4226 . . . . . . . . . 10  |-  ( <.
m ,  u >.  e. 
U. ran  h  <->  E. v  e.  ran  h <. m ,  u >.  e.  v
)
214211, 142opeldm 5058 . . . . . . . . . . . . . . 15  |-  ( <.
m ,  u >.  e.  v  ->  m  e.  dom  v )
215214a1i 11 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  v  ->  m  e.  dom  v ) )
216134, 44syl6ss 3482 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) } )
217 ssel 3464 . . . . . . . . . . . . . . . 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 ) } ) )
218 vex 3090 . . . . . . . . . . . . . . . . . 18  |-  v  e. 
_V
219 dmeq 5055 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  v  ->  dom  s  =  dom  v )
220219eleq2d 2499 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  v ) )
221219eleq1d 2498 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( dom  s  e.  om  <->  dom  v  e.  om )
)
222220, 221anbi12d 715 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  v  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) ) )
223218, 222elab 3224 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) )
224223simprbi 465 . . . . . . . . . . . . . . . 16  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  dom  v  e.  om )
225217, 224syl6 34 . . . . . . . . . . . . . . 15  |-  ( ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  ( v  e.  ran  h  ->  dom  v  e.  om ) )
226216, 225syl 17 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  dom  v  e.  om ) )
227215, 226anim12d 565 . . . . . . . . . . . . 13  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  (
m  e.  dom  v  /\  dom  v  e.  om ) ) )
228 elnn 6716 . . . . . . . . . . . . 13  |-  ( ( m  e.  dom  v  /\  dom  v  e.  om )  ->  m  e.  om )
229227, 228syl6 34 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  m  e.  om ) )
230229expcomd 439 . . . . . . . . . . 11  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  ( <. m ,  u >.  e.  v  ->  m  e.  om )
) )
231230rexlimdv 2922 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( E. v  e. 
ran  h <. m ,  u >.  e.  v  ->  m  e.  om )
)
232213, 231syl5bi 220 . . . . . . . . 9  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  U. ran  h  ->  m  e.  om )
)
233232exlimdv 1771 . . . . . . . 8  |-  ( h : om --> S  -> 
( E. u <. m ,  u >.  e.  U. ran  h  ->  m  e.  om ) )
234212, 233syl5bi 220 . . . . . . 7  |-  ( h : om --> S  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
235234adantr 466 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
236129simpld 460 . . . . . . . . 9  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  m  e.  dom  ( h `  m ) )
237 fnfvelrn 6034 . . . . . . . . . . . . 13  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( h `  m
)  e.  ran  h
)
238 dmeq 5055 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( h `  m )  ->  dom  u  =  dom  ( h `
 m ) )
239238eleq2d 2499 . . . . . . . . . . . . . . 15  |-  ( u  =  ( h `  m )  ->  (
m  e.  dom  u  <->  m  e.  dom  ( h `
 m ) ) )
240239rspcev 3188 . . . . . . . . . . . . . 14  |-  ( ( ( h `  m
)  e.  ran  h  /\  m  e.  dom  ( h `  m
) )  ->  E. u  e.  ran  h  m  e. 
dom  u )
241240ex 435 . . . . . . . . . . . . 13  |-  ( ( h `  m )  e.  ran  h  -> 
( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
242237, 241syl 17 . . . . . . . . . . . 12  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
243147, 242sylan 473 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
244243ancoms 454 . . . . . . . . . 10  |-  ( ( m  e.  om  /\  h : om --> S )  ->  ( m  e. 
dom  ( h `  m )  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
245244adantrr 721 . . . . . . . . 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 ) )
246236, 245mpd 15 . . . . . . . 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 )
247 dmuni 5064 . . . . . . . . . 10  |-  dom  U. ran  h  =  U_ u  e.  ran  h dom  u
248247eleq2i 2507 . . . . . . . . 9  |-  ( m  e.  dom  U. ran  h 
<->  m  e.  U_ u  e.  ran  h dom  u
)
249 eliun 4307 . . . . . . . . 9  |-  ( m  e.  U_ u  e. 
ran  h dom  u  <->  E. u  e.  ran  h  m  e.  dom  u )
250248, 249bitri 252 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u  e.  ran  h  m  e.  dom  u )
251246, 250sylibr 215 . . . . . . 7  |-  ( ( m  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  m  e.  dom  U. ran  h
)
252251expcom 436 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  U. ran  h ) )
253235, 252impbid 193 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  dom  U.
ran  h  <->  m  e.  om ) )
254253eqrdv 2426 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  dom  U. ran  h  =  om )
255 rnuni 5267 . . . . . 6  |-  ran  U. ran  h  =  U_ s  e.  ran  h ran  s
256 frn 5752 . . . . . . . . . . . . . 14  |-  ( s : suc  n --> A  ->  ran  s  C_  A )
2572563ad2ant1 1026 . . . . . . . . . . . . 13  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ran  s  C_  A )
258257rexlimivw 2921 . . . . . . . . . . . 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 )
259258ss2abi 3539 . . . . . . . . . . 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 }
26028, 259eqsstri 3500 . . . . . . . . . 10  |-  S  C_  { s  |  ran  s  C_  A }
261134, 260syl6ss 3482 . . . . . . . . 9  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ran  s  C_  A } )
262 ssel 3464 . . . . . . . . . 10  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  s  e.  { s  |  ran  s  C_  A } ) )
263 abid 2416 . . . . . . . . . 10  |-  ( s  e.  { s  |  ran  s  C_  A } 
<->  ran  s  C_  A
)
264262, 263syl6ib 229 . . . . . . . . 9  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  ran  s  C_  A ) )
265261, 264syl 17 . . . . . . . 8  |-  ( h : om --> S  -> 
( s  e.  ran  h  ->  ran  s  C_  A ) )
266265ralrimiv 2844 . . . . . . 7  |-  ( h : om --> S  ->  A. s  e.  ran  h ran  s  C_  A
)
267 iunss 4343 . . . . . . 7  |-  ( U_ s  e.  ran  h ran  s  C_  A  <->  A. s  e.  ran  h ran  s  C_  A )
268266, 267sylibr 215 . . . . . 6  |-  ( h : om --> S  ->  U_ s  e.  ran  h ran  s  C_  A
)
269255, 268syl5eqss 3514 . . . . 5  |-  ( h : om --> S  ->  ran  U. ran  h  C_  A )
270269adantr 466 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  ran  U. ran  h  C_  A )
271 df-fn 5604 . . . . 5  |-  ( U. ran  h  Fn  om  <->  ( Fun  U.
ran  h  /\  dom  U.
ran  h  =  om ) )
272 df-f 5605 . . . . . 6  |-  ( U. ran  h : om --> A  <->  ( U. ran  h  Fn  om  /\  ran  U. ran  h  C_  A ) )
273272biimpri 209 . . . . 5  |-  ( ( U. ran  h  Fn 
om  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
274271, 273sylanbr 475 . . . 4  |-  ( ( ( Fun  U. ran  h  /\  dom  U. ran  h  =  om )  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
275210, 254, 270, 274syl21anc 1263 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  U. ran  h : om --> A )
276 fnfvelrn 6034 . . . . . . . 8  |-  ( ( h  Fn  om  /\  (/) 
e.  om )  ->  (
h `  (/) )  e. 
ran  h )
277147, 25, 276sylancl 666 . . . . . . 7  |-  ( h : om --> S  -> 
( h `  (/) )  e. 
ran  h )
278277adantr 466 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  e. 
ran  h )
279 elssuni 4251 . . . . . 6  |-  ( ( h `  (/) )  e. 
ran  h  ->  (
h `  (/) )  C_  U.
ran  h )
280278, 279syl 17 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  C_  U.
ran  h )
28154adantr 466 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  (/) 
e.  dom  ( h `  (/) ) )
282 funssfv 5896 . . . . 5  |-  ( ( Fun  U. ran  h  /\  ( h `  (/) )  C_  U.
ran  h  /\  (/)  e.  dom  ( h `  (/) ) )  ->  ( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
283210, 280, 281, 282syl3anc 1264 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
284 simp2 1006 . . . . . . . . . . 11  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
285284rexlimivw 2921 . . . . . . . . . 10  |-  ( E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
286285ss2abi 3539 . . . . . . . . 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 }
28728, 286eqsstri 3500 . . . . . . . 8  |-  S  C_  { s  |  ( s `
 (/) )  =  C }
288134, 287syl6ss 3482 . . . . . . 7  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( s `  (/) )  =  C }
)
289 ssel 3464 . . . . . . . 8  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C } ) )
290 fveq1 5880 . . . . . . . . . 10  |-  ( s  =  ( h `  (/) )  ->  ( s `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
291290eqeq1d 2431 . . . . . . . . 9  |-  ( s  =  ( h `  (/) )  ->  ( (
s `  (/) )  =  C  <->  ( ( h `
 (/) ) `  (/) )  =  C ) )
29246, 291elab 3224 . . . . . . . 8  |-  ( ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C }  <->  ( (
h `  (/) ) `  (/) )  =  C )
293289, 292syl6ib 229 . . . . . . 7  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
294288, 293syl 17 . . . . . 6  |-  ( h : om --> S  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
295294adantr 466 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
296278, 295mpd 15 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) ) `  (/) )  =  C )
297283, 296eqtrd 2470 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  C )
298 nfv 1754 . . . . 5  |-  F/ k  h : om --> S
299 nfra1 2813 . . . . 5  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
300298, 299nfan 1986 . . . 4  |-  F/ k ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
301134ad2antrr 730 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ran  h  C_  S )
302 peano2 6727 . . . . . . . . 9  |-  ( k  e.  om  ->  suc  k  e.  om )
303 fnfvelrn 6034 . . . . . . . . 9  |-  ( ( h  Fn  om  /\  suc  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
304147, 302, 303syl2an 479 . . . . . . . 8  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
305304adantlr 719 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
h `  suc  k )  e.  ran  h )
306236expcom 436 . . . . . . . . 9  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  (
h `  m )
) )
307306ralrimiv 2844 . . . . . . . 8  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  A. m  e.  om  m  e.  dom  ( h `
 m ) )
308 id 23 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  m  =  suc  k )
309 fveq2 5881 . . . . . . . . . . . 12  |-  ( m  =  suc  k  -> 
( h `  m
)  =  ( h `
 suc  k )
)
310309dmeqd 5057 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  dom  ( h `  m
)  =  dom  (
h `  suc  k ) )
311308, 310eleq12d 2511 . . . . . . . . . 10  |-  ( m  =  suc  k  -> 
( m  e.  dom  ( h `  m
)  <->  suc  k  e.  dom  ( h `  suc  k ) ) )
312311rspcv 3184 . . . . . . . . 9  |-  ( suc  k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
313302, 312syl 17 . . . . . . . 8  |-  ( k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
314307, 313mpan9 471 . . . . . . 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 )
)
315 eleq2 2502 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom  s  =  suc  n  ->  ( suc  k  e. 
dom  s  <->  suc  k  e. 
suc  n ) )
316315biimpa 486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( dom  s  =  suc  n  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
31729, 316sylan 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s : suc  n --> A  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
318 ordsucelsuc 6663 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord  n  ->  ( k  e.  n  <->  suc  k  e.  suc  n ) )
31930, 318syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  om  ->  (
k  e.  n  <->  suc  k  e. 
suc  n ) )
320319biimprd 226 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  om  ->  ( suc  k  e.  suc  n  ->  k  e.  n
) )
321 rsp 2798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. k  e.  n  (
s `  suc  k )  e.  ( F `  ( s `  k
) )  ->  (
k  e.  n  -> 
( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) )
322320, 321syl9r 74 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
323322com13 83 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
324317, 323syl 17 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
325324ex 435 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
326325com24 90 . . . . . . . . . . . . . . . 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
) ) ) ) ) )
327326imp 430 . . . . . . . . . . . . . . 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 ) ) ) ) )
3283273adant2 1024 . . . . . . . . . . . . . 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
) ) ) ) )
329328impcom 431 . . . . . . . . . . . . 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 ) ) ) )
330329rexlimiva 2920 . . . . . . . . . . . 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
) ) ) )
331330ss2abi 3539 . . . . . . . . . . 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 ) ) ) }
33228, 331eqsstri 3500 . . . . . . . . . 10  |-  S  C_  { s  |  ( suc  k  e.  dom  s  ->  ( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) }
333 sstr 3478 . . . . . . . . . 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 ) ) ) } )
334332, 333mpan2 675 . . . . . . . . 9  |-  ( ran  h  C_  S  ->  ran  h  C_  { s  |  ( suc  k  e.  dom  s  ->  (
s `  suc  k )  e.  ( F `  ( s `  k
) ) ) } )
335334sseld 3469 . . . . . . . 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 ) ) ) } ) )
336 fvex 5891 . . . . . . . . 9  |-  ( h `
 suc  k )  e.  _V
337 dmeq 5055 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  dom  s  =  dom  ( h `
 suc  k )
)
338337eleq2d 2499 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  ( suc  k  e.  dom  s 
<->  suc  k  e.  dom  ( h `  suc  k ) ) )
339 fveq1 5880 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  (
s `  suc  k )  =  ( ( h `
 suc  k ) `  suc  k ) )
340 fveq1 5880 . . . . . . . . . . . 12  |-  ( s  =  ( h `  suc  k )  ->  (
s `  k )  =  ( ( h `
 suc  k ) `  k ) )
341340fveq2d 5885 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  ( F `  ( s `  k ) )  =  ( F `  (
( h `  suc  k ) `  k
) ) )
342339, 341eleq12d 2511 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  (
( s `  suc  k )  e.  ( F `  ( s `
 k ) )  <-> 
( ( h `  suc  k ) `  suc  k )  e.  ( F `  ( ( h `  suc  k
) `  k )
) ) )
343338, 342imbi12d 321 . . . . . . . . 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 )
) ) ) )
344336, 343elab 3224 . . . . . . . 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 )
) ) )
345335, 344syl6ib 229 . . . . . . 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 )
) ) ) )
346301, 305, 314, 345syl3c 63 . . . . . 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 )
) )
347210adantr 466 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  Fun  U.
ran  h )
348 elssuni 4251 . . . . . . . . . 10  |-  ( ( h `  suc  k
)  e.  ran  h  ->  ( h `  suc  k )  C_  U. ran  h )
349304, 348syl 17 . . . . . . . . 9  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  C_  U. ran  h )
350349adantlr 719 . . . . . . . 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 )
351 funssfv 5896 . . . . . . . 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 ) )
352347, 350, 314, 351syl3anc 1264 . . . . . . 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 ) )
353216sseld 3469 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( h `  suc  k )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } ) )
354337eleq2d 2499 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  suc  k ) ) )
355337eleq1d 2498 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  ( dom  s  e.  om  <->  dom  ( h `  suc  k )  e.  om ) )
356354, 355anbi12d 715 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( h `  suc  k )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
357336, 356elab 3224 . . . . . . . . . . . . . . 15  |-  ( ( h `  suc  k
)  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
358353, 357syl6ib 229 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
359358adantr 466 . . . . . . . . . . . . 13  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
360304, 359mpd 15 . . . . . . . . . . . 12  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
361360simprd 464 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  k  e.  om )  ->  dom  ( h `  suc  k )  e.  om )
362 nnord 6714 . . . . . . . . . . 11  |-  ( dom  ( h `  suc  k )  e.  om  ->  Ord  dom  ( h `  suc  k ) )
363 ordtr 5456 . . . . . . . . . . 11  |-  ( Ord 
dom  ( h `  suc  k )  ->  Tr  dom  ( h `  suc  k ) )
364 trsuc 5526 . . . . . . . . . . . 12  |-  ( ( Tr  dom  ( h `
 suc  k )  /\  suc  k  e.  dom  ( h `  suc  k ) )  -> 
k  e.  dom  (
h `  suc  k ) )
365364ex 435 . . . . . . . . . . 11  |-  ( Tr 
dom  ( h `  suc  k )  ->  ( suc  k  e.  dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
366361, 362, 363, 3654syl 19 . . . . . . . . . 10  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( suc  k  e. 
dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
367366adantlr 719 . . . . . . . . 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 ) ) )
368314, 367mpd 15 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  k  e.  dom  ( h `  suc  k ) )
369 funssfv 5896 . . . . . . . 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
) )
370347, 350, 368, 369syl3anc 1264 . . . . . . 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 )
)
371 simpl 458 . . . . . . . 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 ) )
372 simpr 462 . . . . . . . . 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 ) )
373372fveq2d 5885 . . . . . . . 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
) ) )
374371, 373eleq12d 2511 . . . . . . 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
) ) ) )
375352, 370, 374syl2anc 665 . . . . . 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
) ) ) )
376346, 375mpbird 235 . . . . 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 ) ) )
377376ex 435 . . . 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
) ) ) )
378300, 377ralrimi 2832 . . 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 ) ) )
379 vex 3090 . . . . . 6  |-  h  e. 
_V
380379rnex 6741 . . . . 5  |-  ran  h  e.  _V
381380uniex 6601 . . . 4  |-  U. ran  h  e.  _V
382 feq1 5728 . . . . 5  |-  ( g  =  U. ran  h  ->  ( g : om --> A 
<-> 
U. ran  h : om
--> A ) )
383 fveq1 5880 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( g `  (/) )  =  ( U. ran  h `  (/) ) )
384383eqeq1d 2431 . . . . 5  |-  ( g  =  U. ran  h  ->  ( ( g `  (/) )  =  C  <->  ( U. ran  h `  (/) )  =  C ) )
385 fveq1 5880 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( g `  suc  k )  =  ( U. ran  h `  suc  k ) )
386 fveq1 5880 . . . . . . . 8  |-  ( g  =  U. ran  h  ->  ( g `  k
)  =  ( U. ran  h `  k ) )
387386fveq2d 5885 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( F `  (
g `  k )
)  =  ( F `
 ( U. ran  h `  k )
) )
388385, 387eleq12d 2511 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) ) ) )
389388ralbidv 2871 . . . . 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 ) ) ) )
390382, 384, 3893anbi123d 1335 . . . 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 ) ) ) ) )
391381, 390spcev 3179 . . 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 ) ) ) )
392275, 297, 378, 391syl3anc 1264 . 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 ) ) ) )
393392exlimiv 1769 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 setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    \/ w3o 981    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1870   {cab 2414   A.wral 2782   E.wrex 2783   {crab 2786   _Vcvv 3087    C_ wss 3442   (/)c0 3767   <.cop 4008   U.cuni 4222   U_ciun 4302    |-> cmpt 4484   Tr wtr 4520   dom cdm 4854   ran crn 4855    |` cres 4856   Ord word 5441   suc csuc 5444   Fun wfun 5595    Fn wfn 5596   -->wf 5597   ` cfv 5601   omcom 6706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-dc 8874
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609  df-om 6707  df-1o 7190
This theorem is referenced by:  axdc3lem4  8881
  Copyright terms: Public domain W3C validator