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

Theorem axdc3lem2 8623
Description: Lemma for axdc3 8626. 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 8618 (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 8618 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 22 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  m  =  (/) )
2 fveq2 5694 . . . . . . . . . . . . . 14  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
32dmeqd 5045 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  dom  (
h `  m )  =  dom  ( h `  (/) ) )
41, 3eleq12d 2511 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( m  e.  dom  ( h `
 m )  <->  (/)  e.  dom  ( h `  (/) ) ) )
5 eleq2 2504 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( j  e.  m  <->  j  e.  (/) ) )
62sseq2d 3387 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( ( h `  j ) 
C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  (/) ) ) )
75, 6imbi12d 320 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( ( j  e.  m  -> 
( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) ) ) )
84, 7anbi12d 710 . . . . . . . . . . 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 22 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  m  =  i )
10 fveq2 5694 . . . . . . . . . . . . . 14  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
1110dmeqd 5045 . . . . . . . . . . . . 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 1761 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
j  e.  m  <->  j  e.  i ) )
1410sseq2d 3387 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  i )
) )
1513, 14imbi12d 320 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
( j  e.  m  ->  ( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  i  ->  ( h `
 j )  C_  ( h `  i
) ) ) )
1612, 15anbi12d 710 . . . . . . . . . . 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 22 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  m  =  suc  i )
18 fveq2 5694 . . . . . . . . . . . . . 14  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
1918dmeqd 5045 . . . . . . . . . . . . 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 2504 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( j  e.  m  <->  j  e.  suc  i ) )
2218sseq2d 3387 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( ( h `  j )  C_  (
h `  m )  <->  ( h `  j ) 
C_  ( h `  suc  i ) ) )
2321, 22imbi12d 320 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( ( j  e.  m  ->  ( h `  j )  C_  (
h `  m )
)  <->  ( j  e. 
suc  i  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
2420, 23anbi12d 710 . . . . . . . . . . 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 6498 . . . . . . . . . . . . . . 15  |-  (/)  e.  om
26 ffvelrn 5844 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  (/) 
e.  om )  ->  (
h `  (/) )  e.  S )
2725, 26mpan2 671 . . . . . . . . . . . . . 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 5566 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s : suc  n --> A  ->  dom  s  =  suc  n )
30 nnord 6487 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  om  ->  Ord  n )
31 0elsuc 6449 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord  n  ->  (/)  e.  suc  n )
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  (/)  e.  suc  n )
33 peano2 6499 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  suc  n  e.  om )
34 eleq2 2504 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s 
<->  (/)  e.  suc  n ) )
35 eleq1 2503 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( dom  s  e. 
om 
<->  suc  n  e.  om ) )
3634, 35anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  s  =  suc  n  ->  ( ( (/)  e.  dom  s  /\  dom  s  e. 
om )  <->  ( (/)  e.  suc  n  /\  suc  n  e. 
om ) ) )
3736biimprcd 225 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
(/)  e.  suc  n  /\  suc  n  e.  om )  ->  ( dom  s  =  suc  n  ->  ( (/) 
e.  dom  s  /\  dom  s  e.  om ) ) )
3832, 33, 37syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  om  ->  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
3929, 38syl5com 30 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s : suc  n --> A  -> 
( n  e.  om  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
40393ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . . . . . . . . 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 2839 . . . . . . . . . . . . . . . . . . 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 3427 . . . . . . . . . . . . . . . . . 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 3389 . . . . . . . . . . . . . . . . 17  |-  S  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) }
4544sseli 3355 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e.  S  ->  ( h `  (/) )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } )
46 fvex 5704 . . . . . . . . . . . . . . . . 17  |-  ( h `
 (/) )  e.  _V
47 dmeq 5043 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  ( h `  (/) )  ->  dom  s  =  dom  ( h `  (/) ) )
4847eleq2d 2510 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( (/)  e.  dom  s 
<->  (/)  e.  dom  ( h `
 (/) ) ) )
4947eleq1d 2509 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( dom  s  e.  om  <->  dom  ( h `
 (/) )  e.  om ) )
5048, 49anbi12d 710 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  (/) )  ->  ( ( (/) 
e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) ) )
5146, 50elab 3109 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e. 
{ s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) }  <->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5245, 51sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( h `  (/) )  e.  S  ->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5352simpld 459 . . . . . . . . . . . . . 14  |-  ( ( h `  (/) )  e.  S  ->  (/)  e.  dom  ( h `  (/) ) )
5427, 53syl 16 . . . . . . . . . . . . 13  |-  ( h : om --> S  ->  (/) 
e.  dom  ( h `  (/) ) )
55 noel 3644 . . . . . . . . . . . . . 14  |-  -.  j  e.  (/)
5655pm2.21i 131 . . . . . . . . . . . . 13  |-  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) )
5754, 56jctir 538 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) )
5857adantr 465 . . . . . . . . . . 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 5844 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  i  e.  om )  ->  ( h `  i
)  e.  S )
6059ancoms 453 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  h : om --> S )  ->  ( h `  i )  e.  S
)
6160adantrr 716 . . . . . . . . . . . . 13  |-  ( ( i  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
h `  i )  e.  S )
62 suceq 4787 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  suc  k  =  suc  i )
6362fveq2d 5698 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
64 fveq2 5694 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
6564fveq2d 5698 . . . . . . . . . . . . . . . 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 3074 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )
6867adantrl 715 . . . . . . . . . . . . 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 3355 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  S  ->  (
h `  i )  e.  { s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) } )
70 fvex 5704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h `
 i )  e. 
_V
71 dmeq 5043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( h `  i )  ->  dom  s  =  dom  ( h `
 i ) )
7271eleq2d 2510 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  i
) ) )
7371eleq1d 2509 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( dom  s  e.  om  <->  dom  ( h `  i
)  e.  om )
)
7472, 73anbi12d 710 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( h `  i )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) ) )
7570, 74elab 3109 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) )
7669, 75sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  i )  e.  S  ->  ( (/) 
e.  dom  ( h `  i )  /\  dom  ( h `  i
)  e.  om )
)
7776simprd 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  i )  e.  S  ->  dom  ( h `  i
)  e.  om )
78 nnord 6487 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( h `  i
)  e.  om  ->  Ord 
dom  ( h `  i ) )
79 ordsucelsuc 6436 . . . . . . . . . . . . . . . . . 18  |-  ( Ord 
dom  ( h `  i )  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8077, 78, 793syl 20 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  i )  e.  S  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8180adantr 465 . . . . . . . . . . . . . . . 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 5043 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( h `  i )  ->  dom  x  =  dom  ( h `
 i ) )
83 suceq 4787 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  x  =  dom  (
h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i ) )
8482, 83syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  suc  dom  x  =  suc  dom  ( h `  i
) )
8584eqeq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  ( dom  y  =  suc  dom  x  <->  dom  y  =  suc  dom  ( h `  i
) ) )
8682reseq2d 5113 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  (
y  |`  dom  x )  =  ( y  |`  dom  ( h `  i
) ) )
87 id 22 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  x  =  ( h `  i ) )
8886, 87eqeq12d 2457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  (
( y  |`  dom  x
)  =  x  <->  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) )
8985, 88anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . 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 2967 . . . . . . . . . . . . . . . . . . . . . 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 8622 . . . . . . . . . . . . . . . . . . . . . . 23  |-  S  e. 
_V
9493rabex 4446 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i
)  /\  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) }  e.  _V
9590, 91, 94fvmpt 5777 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  i )  e.  S  ->  ( G `  ( h `  i ) )  =  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i )  /\  (
y  |`  dom  ( h `
 i ) )  =  ( h `  i ) ) } )
9695eleq2d 2510 . . . . . . . . . . . . . . . . . . . 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 5043 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  dom  y  =  dom  ( h `
 suc  i )
)
9897eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  ( dom  y  =  suc  dom  ( h `  i
)  <->  dom  ( h `  suc  i )  =  suc  dom  ( h `  i
) ) )
99 reseq1 5107 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  (
y  |`  dom  ( h `
 i ) )  =  ( ( h `
 suc  i )  |` 
dom  ( h `  i ) ) )
10099eqeq1d 2451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  (
( y  |`  dom  (
h `  i )
)  =  ( h `
 i )  <->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) ) )
10198, 100anbi12d 710 . . . . . . . . . . . . . . . . . . . . 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 3120 . . . . . . . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . . . . . . . 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 624 . . . . . . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  dom  ( h `
 suc  i )  =  suc  dom  ( h `  i ) )
106105eleq2d 2510 . . . . . . . . . . . . . . . 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 256 . . . . . . . . . . . . . . 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 207 . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) )
110 resss 5137 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  i
)  |`  dom  ( h `
 i ) ) 
C_  ( h `  suc  i )
111 sseq1 3380 . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  suc  i )  |`  dom  (
h `  i )
)  =  ( h `
 i )  -> 
( h `  i
)  C_  ( h `  suc  i ) )
113 elsuci 4788 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  suc  i  -> 
( j  e.  i  \/  j  =  i ) )
114 pm2.27 39 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( h `  j )  C_  (
h `  i )
) )
115 sstr2 3366 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  j ) 
C_  ( h `  i )  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
116114, 115syl6 33 . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  (
h `  j )  =  ( h `  i ) )
118117sseq1d 3386 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
( h `  j
)  C_  ( h `  suc  i )  <->  ( h `  i )  C_  (
h `  suc  i ) ) )
119118biimprd 223 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
120119a1d 25 . . . . . . . . . . . . . . . . . 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 379 . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . 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 80 . . . . . . . . . . . . . . 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 20 . . . . . . . . . . . . . 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 563 . . . . . . . . . . . . 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 661 . . . . . . . . . . . 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 434 . . . . . . . . . . 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 6507 . . . . . . . . . 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 429 . . . . . . . . 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 463 . . . . . . . 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 435 . . . . . . 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 2808 . . . . . 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 2801 . . . . 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 5568 . . . . . . . . . . . 12  |-  ( h : om --> S  ->  ran  h  C_  S )
135 ffun 5564 . . . . . . . . . . . . . . . 16  |-  ( s : suc  n --> A  ->  Fun  s )
1361353ad2ant1 1009 . . . . . . . . . . . . . . 15  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  Fun  s )
137136rexlimivw 2840 . . . . . . . . . . . . . 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 3427 . . . . . . . . . . . . 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 3389 . . . . . . . . . . . 12  |-  S  C_  { s  |  Fun  s }
140134, 139syl6ss 3371 . . . . . . . . . . 11  |-  ( h : om --> S  ->  ran  h  C_  { s  |  Fun  s } )
141140sseld 3358 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  u  e.  {
s  |  Fun  s } ) )
142 vex 2978 . . . . . . . . . . 11  |-  u  e. 
_V
143 funeq 5440 . . . . . . . . . . 11  |-  ( s  =  u  ->  ( Fun  s  <->  Fun  u ) )
144142, 143elab 3109 . . . . . . . . . 10  |-  ( u  e.  { s  |  Fun  s }  <->  Fun  u )
145141, 144syl6ib 226 . . . . . . . . 9  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  Fun  u )
)
146145adantr 465 . . . . . . . 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 5562 . . . . . . . . 9  |-  ( h : om --> S  ->  h  Fn  om )
148 fvelrnb 5742 . . . . . . . . . . . . 13  |-  ( h  Fn  om  ->  (
v  e.  ran  h  <->  E. b  e.  om  (
h `  b )  =  v ) )
149 fvelrnb 5742 . . . . . . . . . . . . . . 15  |-  ( h  Fn  om  ->  (
u  e.  ran  h  <->  E. a  e.  om  (
h `  a )  =  u ) )
150 nnord 6487 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  e.  om  ->  Ord  a )
151 nnord 6487 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  om  ->  Ord  b )
152150, 151anim12i 566 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  om  /\  b  e.  om )  ->  ( Ord  a  /\  Ord  b ) )
153 ordtri3or 4754 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Ord  a  /\  Ord  b )  ->  (
a  e.  b  \/  a  =  b  \/  b  e.  a ) )
154 fveq2 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  b  ->  (
h `  m )  =  ( h `  b ) )
155154sseq2d 3387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  b  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  b )
) )
156155raleqbi1dv 2928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  b  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  b  ( h `  j )  C_  (
h `  b )
) )
157156rspcv 3072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  a  ->  (
h `  j )  =  ( h `  a ) )
159158sseq1d 3386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  a  ->  (
( h `  j
)  C_  ( h `  b )  <->  ( h `  a )  C_  (
h `  b )
) )
160159rspccv 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  b  (
h `  j )  C_  ( h `  b
)  ->  ( a  e.  b  ->  ( h `
 a )  C_  ( h `  b
) ) )
161157, 160syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 392 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . . 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 79 . . . . . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  b  ->  (
h `  a )  =  ( h `  b ) )
168 eqimss 3411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  a )  =  ( h `  b )  ->  (
h `  a )  C_  ( h `  b
) )
169168orcd 392 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( h `  a )  =  ( h `  b )  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
170167, 169syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  b  ->  (
( h `  a
)  C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) ) )
171170a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  a  ->  (
h `  m )  =  ( h `  a ) )
174173sseq2d 3387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  a  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  a )
) )
175174raleqbi1dv 2928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  a  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  a  ( h `  j )  C_  (
h `  a )
) )
176175rspcv 3072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  b  ->  (
h `  j )  =  ( h `  b ) )
178177sseq1d 3386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  b  ->  (
( h `  j
)  C_  ( h `  a )  <->  ( h `  b )  C_  (
h `  a )
) )
179178rspccv 3073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  a  (
h `  j )  C_  ( h `  a
)  ->  ( b  e.  a  ->  ( h `
 b )  C_  ( h `  a
) ) )
180176, 179syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 393 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . . . . . . . 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 79 . . . . . . . . . . . . . . . . . . . . . . . 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 1281 . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . 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 36 . . . . . . . . . . . . . . . . . . . . 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 3382 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 a )  C_  ( h `  b
)  <->  u  C_  v ) )
190 sseq12 3382 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h `  b
)  =  v  /\  ( h `  a
)  =  u )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
191190ancoms 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
192189, 191orbi12d 709 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( ( h `  a ) 
C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  <->  ( u  C_  v  \/  v  C_  u ) ) )
193192biimpcd 224 . . . . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . . . . . . . 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 607 . . . . . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . . . . . 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 2838 . . . . . . . . . . . . . . . 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 2843 . . . . . . . . . . . . . . 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 228 . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . 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 215 . . . . . . . . . . . 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 87 . . . . . . . . . . 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 429 . . . . . . . . . 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 2808 . . . . . . . . 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 471 . . . . . . . 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 533 . . . . . . 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 2801 . . . . . 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 5487 . . . . . 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 16 . . . . 5  |-  ( ( h : om --> S  /\  A. m  e.  om  A. j  e.  m  (
h `  j )  C_  ( h `  m
) )  ->  Fun  U.
ran  h )
211133, 210syldan 470 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  Fun  U. ran  h )
212 vex 2978 . . . . . . . . 9  |-  m  e. 
_V
213212eldm2 5041 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u <. m ,  u >.  e.  U. ran  h )
214 eluni2 4098 . . . . . . . . . 10  |-  ( <.
m ,  u >.  e. 
U. ran  h  <->  E. v  e.  ran  h <. m ,  u >.  e.  v
)
215212, 142opeldm 5046 . . . . . . . . . . . . . . 15  |-  ( <.
m ,  u >.  e.  v  ->  m  e.  dom  v )
216215a1i 11 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  v  ->  m  e.  dom  v ) )
217134, 44syl6ss 3371 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) } )
218 ssel 3353 . . . . . . . . . . . . . . . 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 2978 . . . . . . . . . . . . . . . . . 18  |-  v  e. 
_V
220 dmeq 5043 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  v  ->  dom  s  =  dom  v )
221220eleq2d 2510 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  v ) )
222220eleq1d 2509 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( dom  s  e.  om  <->  dom  v  e.  om )
)
223221, 222anbi12d 710 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  v  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) ) )
224219, 223elab 3109 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) )
225224simprbi 464 . . . . . . . . . . . . . . . 16  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  dom  v  e.  om )
226218, 225syl6 33 . . . . . . . . . . . . . . 15  |-  ( ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  ( v  e.  ran  h  ->  dom  v  e.  om ) )
227217, 226syl 16 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  dom  v  e.  om ) )
228216, 227anim12d 563 . . . . . . . . . . . . 13  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  (
m  e.  dom  v  /\  dom  v  e.  om ) ) )
229 elnn 6489 . . . . . . . . . . . . 13  |-  ( ( m  e.  dom  v  /\  dom  v  e.  om )  ->  m  e.  om )
230228, 229syl6 33 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  m  e.  om ) )
231230expcomd 438 . . . . . . . . . . 11  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  ( <. m ,  u >.  e.  v  ->  m  e.  om )
) )
232231rexlimdv 2843 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( E. v  e. 
ran  h <. m ,  u >.  e.  v  ->  m  e.  om )
)
233214, 232syl5bi 217 . . . . . . . . 9  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  U. ran  h  ->  m  e.  om )
)
234233exlimdv 1690 . . . . . . . 8  |-  ( h : om --> S  -> 
( E. u <. m ,  u >.  e.  U. ran  h  ->  m  e.  om ) )
235213, 234syl5bi 217 . . . . . . 7  |-  ( h : om --> S  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
236235adantr 465 . . . . . 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 459 . . . . . . . . 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 5843 . . . . . . . . . . . . 13  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( h `  m
)  e.  ran  h
)
239 dmeq 5043 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( h `  m )  ->  dom  u  =  dom  ( h `
 m ) )
240239eleq2d 2510 . . . . . . . . . . . . . . 15  |-  ( u  =  ( h `  m )  ->  (
m  e.  dom  u  <->  m  e.  dom  ( h `
 m ) ) )
241240rspcev 3076 . . . . . . . . . . . . . 14  |-  ( ( ( h `  m
)  e.  ran  h  /\  m  e.  dom  ( h `  m
) )  ->  E. u  e.  ran  h  m  e. 
dom  u )
242241ex 434 . . . . . . . . . . . . 13  |-  ( ( h `  m )  e.  ran  h  -> 
( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
243238, 242syl 16 . . . . . . . . . . . 12  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
244147, 243sylan 471 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
245244ancoms 453 . . . . . . . . . 10  |-  ( ( m  e.  om  /\  h : om --> S )  ->  ( m  e. 
dom  ( h `  m )  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
246245adantrr 716 . . . . . . . . 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 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 )
248 dmuni 5052 . . . . . . . . . 10  |-  dom  U. ran  h  =  U_ u  e.  ran  h dom  u
249248eleq2i 2507 . . . . . . . . 9  |-  ( m  e.  dom  U. ran  h 
<->  m  e.  U_ u  e.  ran  h dom  u
)
250 eliun 4178 . . . . . . . . 9  |-  ( m  e.  U_ u  e. 
ran  h dom  u  <->  E. u  e.  ran  h  m  e.  dom  u )
251249, 250bitri 249 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u  e.  ran  h  m  e.  dom  u )
252247, 251sylibr 212 . . . . . . 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 435 . . . . . 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 191 . . . . 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 2441 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  dom  U. ran  h  =  om )
256 rnuni 5251 . . . . . 6  |-  ran  U. ran  h  =  U_ s  e.  ran  h ran  s
257 frn 5568 . . . . . . . . . . . . . 14  |-  ( s : suc  n --> A  ->  ran  s  C_  A )
2582573ad2ant1 1009 . . . . . . . . . . . . 13  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ran  s  C_  A )
259258rexlimivw 2840 . . . . . . . . . . . 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 3427 . . . . . . . . . . 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 3389 . . . . . . . . . 10  |-  S  C_  { s  |  ran  s  C_  A }
262134, 261syl6ss 3371 . . . . . . . . 9  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ran  s  C_  A } )
263 ssel 3353 . . . . . . . . . 10  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  s  e.  { s  |  ran  s  C_  A } ) )
264 abid 2431 . . . . . . . . . 10  |-  ( s  e.  { s  |  ran  s  C_  A } 
<->  ran  s  C_  A
)
265263, 264syl6ib 226 . . . . . . . . 9  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  ran  s  C_  A ) )
266262, 265syl 16 . . . . . . . 8  |-  ( h : om --> S  -> 
( s  e.  ran  h  ->  ran  s  C_  A ) )
267266ralrimiv 2801 . . . . . . 7  |-  ( h : om --> S  ->  A. s  e.  ran  h ran  s  C_  A
)
268 iunss 4214 . . . . . . 7  |-  ( U_ s  e.  ran  h ran  s  C_  A  <->  A. s  e.  ran  h ran  s  C_  A )
269267, 268sylibr 212 . . . . . 6  |-  ( h : om --> S  ->  U_ s  e.  ran  h ran  s  C_  A
)
270256, 269syl5eqss 3403 . . . . 5  |-  ( h : om --> S  ->  ran  U. ran  h  C_  A )
271270adantr 465 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  ran  U. ran  h  C_  A )
272 df-fn 5424 . . . . 5  |-  ( U. ran  h  Fn  om  <->  ( Fun  U.
ran  h  /\  dom  U.
ran  h  =  om ) )
273 df-f 5425 . . . . . 6  |-  ( U. ran  h : om --> A  <->  ( U. ran  h  Fn  om  /\  ran  U. ran  h  C_  A ) )
274273biimpri 206 . . . . 5  |-  ( ( U. ran  h  Fn 
om  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
275272, 274sylanbr 473 . . . 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 1217 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  U. ran  h : om --> A )
277 fnfvelrn 5843 . . . . . . . 8  |-  ( ( h  Fn  om  /\  (/) 
e.  om )  ->  (
h `  (/) )  e. 
ran  h )
278147, 25, 277sylancl 662 . . . . . . 7  |-  ( h : om --> S  -> 
( h `  (/) )  e. 
ran  h )
279278adantr 465 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  e. 
ran  h )
280 elssuni 4124 . . . . . 6  |-  ( ( h `  (/) )  e. 
ran  h  ->  (
h `  (/) )  C_  U.
ran  h )
281279, 280syl 16 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  C_  U.
ran  h )
28254adantr 465 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  (/) 
e.  dom  ( h `  (/) ) )
283 funssfv 5708 . . . . 5  |-  ( ( Fun  U. ran  h  /\  ( h `  (/) )  C_  U.
ran  h  /\  (/)  e.  dom  ( h `  (/) ) )  ->  ( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
284211, 281, 282, 283syl3anc 1218 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
285 simp2 989 . . . . . . . . . . 11  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
286285rexlimivw 2840 . . . . . . . . . 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 3427 . . . . . . . . 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 3389 . . . . . . . 8  |-  S  C_  { s  |  ( s `
 (/) )  =  C }
289134, 288syl6ss 3371 . . . . . . 7  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( s `  (/) )  =  C }
)
290 ssel 3353 . . . . . . . 8  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C } ) )
291 fveq1 5693 . . . . . . . . . 10  |-  ( s  =  ( h `  (/) )  ->  ( s `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
292291eqeq1d 2451 . . . . . . . . 9  |-  ( s  =  ( h `  (/) )  ->  ( (
s `  (/) )  =  C  <->  ( ( h `
 (/) ) `  (/) )  =  C ) )
29346, 292elab 3109 . . . . . . . 8  |-  ( ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C }  <->  ( (
h `  (/) ) `  (/) )  =  C )
294290, 293syl6ib 226 . . . . . . 7  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
295289, 294syl 16 . . . . . 6  |-  ( h : om --> S  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
296295adantr 465 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) )  e.  ran  h  ->  ( ( h `  (/) ) `  (/) )  =  C ) )
297279, 296mpd 15 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( ( h `  (/) ) `  (/) )  =  C )
298284, 297eqtrd 2475 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  C )
299 nfv 1673 . . . . 5  |-  F/ k  h : om --> S
300 nfra1 2769 . . . . 5  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
301299, 300nfan 1861 . . . 4  |-  F/ k ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
302134ad2antrr 725 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ran  h  C_  S )
303 peano2 6499 . . . . . . . . 9  |-  ( k  e.  om  ->  suc  k  e.  om )
304 fnfvelrn 5843 . . . . . . . . 9  |-  ( ( h  Fn  om  /\  suc  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
305147, 303, 304syl2an 477 . . . . . . . 8  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
306305adantlr 714 . . . . . . 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 435 . . . . . . . . 9  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  (
h `  m )
) )
308307ralrimiv 2801 . . . . . . . 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 22 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  m  =  suc  k )
310 fveq2 5694 . . . . . . . . . . . 12  |-  ( m  =  suc  k  -> 
( h `  m
)  =  ( h `
 suc  k )
)
311310dmeqd 5045 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  dom  ( h `  m
)  =  dom  (
h `  suc  k ) )
312309, 311eleq12d 2511 . . . . . . . . . 10  |-  ( m  =  suc  k  -> 
( m  e.  dom  ( h `  m
)  <->  suc  k  e.  dom  ( h `  suc  k ) ) )
313312rspcv 3072 . . . . . . . . 9  |-  ( suc  k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
314303, 313syl 16 . . . . . . . 8  |-  ( k  e.  om  ->  ( A. m  e.  om  m  e.  dom  ( h `
 m )  ->  suc  k  e.  dom  ( h `  suc  k ) ) )
315308, 314mpan9 469 . . . . . . 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 2504 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom  s  =  suc  n  ->  ( suc  k  e. 
dom  s  <->  suc  k  e. 
suc  n ) )
317316biimpa 484 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( dom  s  =  suc  n  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
31829, 317sylan 471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s : suc  n --> A  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
319 ordsucelsuc 6436 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( Ord  n  ->  ( k  e.  n  <->  suc  k  e.  suc  n ) )
32030, 319syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  om  ->  (
k  e.  n  <->  suc  k  e. 
suc  n ) )
321320biimprd 223 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  om  ->  ( suc  k  e.  suc  n  ->  k  e.  n
) )
322 rsp 2779 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. k  e.  n  (
s `  suc  k )  e.  ( F `  ( s `  k
) )  ->  (
k  e.  n  -> 
( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) )
323321, 322syl9r 72 . . . . . . . . . . . . . . . . . . . 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 80 . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . 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 87 . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . 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 430 . . . . . . . . . . . . 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 2839 . . . . . . . . . . . 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 3427 . . . . . . . . . . 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 3389 . . . . . . . . . 10  |-  S  C_  { s  |  ( suc  k  e.  dom  s  ->  ( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) }
334 sstr 3367 . . . . . . . . . 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 671 . . . . . . . . 9  |-  ( ran  h  C_  S  ->  ran  h  C_  { s  |  ( suc  k  e.  dom  s  ->  (
s `  suc  k )  e.  ( F `  ( s `  k
) ) ) } )
336335sseld 3358 . . . . . . . 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 5704 . . . . . . . . 9  |-  ( h `
 suc  k )  e.  _V
338 dmeq 5043 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  dom  s  =  dom  ( h `
 suc  k )
)
339338eleq2d 2510 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  ( suc  k  e.  dom  s 
<->  suc  k  e.  dom  ( h `  suc  k ) ) )
340 fveq1 5693 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  (
s `  suc  k )  =  ( ( h `
 suc  k ) `  suc  k ) )
341 fveq1 5693 . . . . . . . . . . . 12  |-  ( s  =  ( h `  suc  k )  ->  (
s `  k )  =  ( ( h `
 suc  k ) `  k ) )
342341fveq2d 5698 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  ( F `  ( s `  k ) )  =  ( F `  (
( h `  suc  k ) `  k
) ) )
343340, 342eleq12d 2511 . . . . . . . . . 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 320 . . . . . . . . 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 3109 . . . . . . . 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 226 . . . . . . 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 61 . . . . . 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 465 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  Fun  U.
ran  h )
349 elssuni 4124 . . . . . . . . . 10  |-  ( ( h `  suc  k
)  e.  ran  h  ->  ( h `  suc  k )  C_  U. ran  h )
350305, 349syl 16 . . . . . . . . 9  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  C_  U. ran  h )
351350adantlr 714 . . . . . . . 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 5708 . . . . . . . 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 1218 . . . . . . 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 3358 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( h `  suc  k )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } ) )
355338eleq2d 2510 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  suc  k ) ) )
356338eleq1d 2509 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  ( dom  s  e.  om  <->  dom  ( h `  suc  k )  e.  om ) )
357355, 356anbi12d 710 . . . . . . . . . . . . . . . 16  |-  ( s  =  ( h `  suc  k )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
358337, 357elab 3109 . . . . . . . . . . . . . . 15  |-  ( ( 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 226 . . . . . . . . . . . . . 14  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
360359adantr 465 . . . . . . . . . . . . 13  |-  ( ( 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 15 . . . . . . . . . . . 12  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
362361simprd 463 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  k  e.  om )  ->  dom  ( h `  suc  k )  e.  om )
363 nnord 6487 . . . . . . . . . . 11  |-  ( dom  ( h `  suc  k )  e.  om  ->  Ord  dom  ( h `  suc  k ) )
364 ordtr 4736 . . . . . . . . . . 11  |-  ( Ord 
dom  ( h `  suc  k )  ->  Tr  dom  ( h `  suc  k ) )
365 trsuc 4806 . . . . . . . . . . . 12  |-  ( ( Tr  dom  ( h `
 suc  k )  /\  suc  k  e.  dom  ( h `  suc  k ) )  -> 
k  e.  dom  (
h `  suc  k ) )
366365ex 434 . . . . . . . . . . 11  |-  ( Tr 
dom  ( h `  suc  k )  ->  ( suc  k  e.  dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
367362, 363, 364, 3664syl 21 . . . . . . . . . 10  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( suc  k  e. 
dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
368367adantlr 714 . . . . . . . . 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 ) ) )
369315, 368mpd 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 ) )
370 funssfv 5708 . . . . . . . 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
) )
371348, 351, 369, 370syl3anc 1218 . . . . . . 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 )
)
372 simpl 457 . . . . . . . 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 ) )
373 simpr 461 . . . . . . . . 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 ) )
374373fveq2d 5698 . . . . . . . 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
) ) )
375372, 374eleq12d 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
) ) ) )
376353, 371, 375syl2anc 661 . . . . . 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
) ) ) )
377347, 376mpbird 232 . . . . 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 ) ) )
378377ex 434 . . . 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
) ) ) )
379301, 378ralrimi 2800 . . 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 ) ) )
380 vex 2978 . . . . . 6  |-  h  e. 
_V
381380rnex 6515 . . . . 5  |-  ran  h  e.  _V
382381uniex 6379 . . . 4  |-  U. ran  h  e.  _V
383 feq1 5545 . . . . 5  |-  ( g  =  U. ran  h  ->  ( g : om --> A 
<-> 
U. ran  h : om
--> A ) )
384 fveq1 5693 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( g `  (/) )  =  ( U. ran  h `  (/) ) )
385384eqeq1d 2451 . . . . 5  |-  ( g  =  U. ran  h  ->  ( ( g `  (/) )  =  C  <->  ( U. ran  h `  (/) )  =  C ) )
386 fveq1 5693 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( g `  suc  k )  =  ( U. ran  h `  suc  k ) )
387 fveq1 5693 . . . . . . . 8  |-  ( g  =  U. ran  h  ->  ( g `  k
)  =  ( U. ran  h `  k ) )
388387fveq2d 5698 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( F `  (
g `  k )
)  =  ( F `
 ( U. ran  h `  k )
) )
389386, 388eleq12d 2511 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) ) ) )
390389ralbidv 2738 . . . . 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 ) ) ) )
391383, 385, 3903anbi123d 1289 . . . 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 ) ) ) ) )
392382, 391spcev 3067 . . 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 ) ) ) )
393276, 298, 379, 392syl3anc 1218 . 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 ) ) ) )
394393exlimiv 1688 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 184    \/ wo 368    /\ wa 369    \/ w3o 964    /\ w3a 965    = wceq 1369   E.wex 1586    e. wcel 1756   {cab 2429   A.wral 2718   E.wrex 2719   {crab 2722   _Vcvv 2975    C_ wss 3331   (/)c0 3640   <.cop 3886   U.cuni 4094   U_ciun 4174    e. cmpt 4353   Tr wtr 4388   Ord word 4721   suc csuc 4724   dom cdm 4843   ran crn 4844    |` cres 4845   Fun wfun 5415    Fn wfn 5416   -->wf 5417   ` cfv 5421   omcom 6479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pow 4473  ax-pr 4534  ax-un 6375  ax-dc 8618
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-sbc 3190  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-pss 3347  df-nul 3641  df-if 3795  df-pw 3865  df-sn 3881  df-pr 3883  df-tp 3885  df-op 3887  df-uni 4095  df-iun 4176  df-br 4296  df-opab 4354  df-mpt 4355  df-tr 4389  df-eprel 4635  df-id 4639  df-po 4644  df-so 4645  df-fr 4682  df-we 4684  df-ord 4725  df-on 4726  df-lim 4727  df-suc 4728  df-xp 4849  df-rel 4850  df-cnv 4851  df-co 4852  df-dm 4853  df-rn 4854  df-res 4855  df-iota 5384  df-fun 5423  df-fn 5424  df-f 5425  df-fv 5429  df-om 6480  df-1o 6923
This theorem is referenced by:  axdc3lem4  8625
  Copyright terms: Public domain W3C validator