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

Theorem axdc3lem2 8323
Description: Lemma for axdc3 8326. 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 8318 (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 8318 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 20 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  m  =  (/) )
2 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( m  =  (/)  ->  ( h `
 m )  =  ( h `  (/) ) )
32dmeqd 5064 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  dom  (
h `  m )  =  dom  ( h `  (/) ) )
41, 3eleq12d 2503 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( m  e.  dom  ( h `
 m )  <->  (/)  e.  dom  ( h `  (/) ) ) )
5 eleq2 2496 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( j  e.  m  <->  j  e.  (/) ) )
62sseq2d 3368 . . . . . . . . . . . . 13  |-  ( m  =  (/)  ->  ( ( h `  j ) 
C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  (/) ) ) )
75, 6imbi12d 312 . . . . . . . . . . . 12  |-  ( m  =  (/)  ->  ( ( j  e.  m  -> 
( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) ) ) )
84, 7anbi12d 692 . . . . . . . . . . 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 20 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  m  =  i )
10 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( m  =  i  ->  (
h `  m )  =  ( h `  i ) )
1110dmeqd 5064 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  dom  ( h `  m
)  =  dom  (
h `  i )
)
129, 11eleq12d 2503 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
m  e.  dom  (
h `  m )  <->  i  e.  dom  ( h `
 i ) ) )
13 elequ2 1730 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
j  e.  m  <->  j  e.  i ) )
1410sseq2d 3368 . . . . . . . . . . . . 13  |-  ( m  =  i  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  i )
) )
1513, 14imbi12d 312 . . . . . . . . . . . 12  |-  ( m  =  i  ->  (
( j  e.  m  ->  ( h `  j
)  C_  ( h `  m ) )  <->  ( j  e.  i  ->  ( h `
 j )  C_  ( h `  i
) ) ) )
1612, 15anbi12d 692 . . . . . . . . . . 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 20 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  m  =  suc  i )
18 fveq2 5720 . . . . . . . . . . . . . 14  |-  ( m  =  suc  i  -> 
( h `  m
)  =  ( h `
 suc  i )
)
1918dmeqd 5064 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  ->  dom  ( h `  m
)  =  dom  (
h `  suc  i ) )
2017, 19eleq12d 2503 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( m  e.  dom  ( h `  m
)  <->  suc  i  e.  dom  ( h `  suc  i ) ) )
21 eleq2 2496 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( j  e.  m  <->  j  e.  suc  i ) )
2218sseq2d 3368 . . . . . . . . . . . . 13  |-  ( m  =  suc  i  -> 
( ( h `  j )  C_  (
h `  m )  <->  ( h `  j ) 
C_  ( h `  suc  i ) ) )
2321, 22imbi12d 312 . . . . . . . . . . . 12  |-  ( m  =  suc  i  -> 
( ( j  e.  m  ->  ( h `  j )  C_  (
h `  m )
)  <->  ( j  e. 
suc  i  ->  (
h `  j )  C_  ( h `  suc  i ) ) ) )
2420, 23anbi12d 692 . . . . . . . . . . 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 4856 . . . . . . . . . . . . . . 15  |-  (/)  e.  om
26 ffvelrn 5860 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  (/) 
e.  om )  ->  (
h `  (/) )  e.  S )
2725, 26mpan2 653 . . . . . . . . . . . . . 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 5587 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s : suc  n --> A  ->  dom  s  =  suc  n )
30 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( n  e.  om  ->  Ord  n )
31 0elsuc 4807 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( Ord  n  ->  (/)  e.  suc  n )
3230, 31syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  (/)  e.  suc  n )
33 peano2 4857 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  om  ->  suc  n  e.  om )
34 eleq2 2496 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s 
<->  (/)  e.  suc  n ) )
35 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( dom  s  =  suc  n  ->  ( dom  s  e. 
om 
<->  suc  n  e.  om ) )
3634, 35anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( dom  s  =  suc  n  ->  ( ( (/)  e.  dom  s  /\  dom  s  e. 
om )  <->  ( (/)  e.  suc  n  /\  suc  n  e. 
om ) ) )
3736biimprcd 217 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
(/)  e.  suc  n  /\  suc  n  e.  om )  ->  ( dom  s  =  suc  n  ->  ( (/) 
e.  dom  s  /\  dom  s  e.  om ) ) )
3832, 33, 37syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  om  ->  ( dom  s  =  suc  n  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
3929, 38syl5com 28 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s : suc  n --> A  -> 
( n  e.  om  ->  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) ) )
40393ad2ant1 978 . . . . . . . . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . . . . . . . . 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 2817 . . . . . . . . . . . . . . . . . . 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 3407 . . . . . . . . . . . . . . . . . 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 3370 . . . . . . . . . . . . . . . . 17  |-  S  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) }
4544sseli 3336 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e.  S  ->  ( h `  (/) )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } )
46 fvex 5734 . . . . . . . . . . . . . . . . 17  |-  ( h `
 (/) )  e.  _V
47 dmeq 5062 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  ( h `  (/) )  ->  dom  s  =  dom  ( h `  (/) ) )
4847eleq2d 2502 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( (/)  e.  dom  s 
<->  (/)  e.  dom  ( h `
 (/) ) ) )
4947eleq1d 2501 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  (/) )  ->  ( dom  s  e.  om  <->  dom  ( h `
 (/) )  e.  om ) )
5048, 49anbi12d 692 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  (/) )  ->  ( ( (/) 
e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) ) )
5146, 50elab 3074 . . . . . . . . . . . . . . . 16  |-  ( ( h `  (/) )  e. 
{ s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) }  <->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5245, 51sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( h `  (/) )  e.  S  ->  ( (/)  e.  dom  ( h `  (/) )  /\  dom  ( h `  (/) )  e. 
om ) )
5352simpld 446 . . . . . . . . . . . . . 14  |-  ( ( h `  (/) )  e.  S  ->  (/)  e.  dom  ( h `  (/) ) )
5427, 53syl 16 . . . . . . . . . . . . 13  |-  ( h : om --> S  ->  (/) 
e.  dom  ( h `  (/) ) )
55 noel 3624 . . . . . . . . . . . . . 14  |-  -.  j  e.  (/)
5655pm2.21i 125 . . . . . . . . . . . . 13  |-  ( j  e.  (/)  ->  ( h `  j )  C_  (
h `  (/) ) )
5754, 56jctir 525 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( (/)  e.  dom  (
h `  (/) )  /\  ( j  e.  (/)  ->  ( h `  j
)  C_  ( h `  (/) ) ) ) )
5857adantr 452 . . . . . . . . . . 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 5860 . . . . . . . . . . . . . . 15  |-  ( ( h : om --> S  /\  i  e.  om )  ->  ( h `  i
)  e.  S )
6059ancoms 440 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  h : om --> S )  ->  ( h `  i )  e.  S
)
6160adantrr 698 . . . . . . . . . . . . 13  |-  ( ( i  e.  om  /\  ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )  ->  (
h `  i )  e.  S )
62 suceq 4638 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  suc  k  =  suc  i )
6362fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  (
h `  suc  k )  =  ( h `  suc  i ) )
64 fveq2 5720 . . . . . . . . . . . . . . . . 17  |-  ( k  =  i  ->  (
h `  k )  =  ( h `  i ) )
6564fveq2d 5724 . . . . . . . . . . . . . . . 16  |-  ( k  =  i  ->  ( G `  ( h `  k ) )  =  ( G `  (
h `  i )
) )
6663, 65eleq12d 2503 . . . . . . . . . . . . . . 15  |-  ( k  =  i  ->  (
( h `  suc  k )  e.  ( G `  ( h `
 k ) )  <-> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) ) )
6766rspcva 3042 . . . . . . . . . . . . . 14  |-  ( ( i  e.  om  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )
6867adantrl 697 . . . . . . . . . . . . 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 3336 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  S  ->  (
h `  i )  e.  { s  |  (
(/)  e.  dom  s  /\  dom  s  e.  om ) } )
70 fvex 5734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( h `
 i )  e. 
_V
71 dmeq 5062 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( s  =  ( h `  i )  ->  dom  s  =  dom  ( h `
 i ) )
7271eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  i
) ) )
7371eleq1d 2501 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( s  =  ( h `  i )  ->  ( dom  s  e.  om  <->  dom  ( h `  i
)  e.  om )
)
7472, 73anbi12d 692 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  ( h `  i )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) ) )
7570, 74elab 3074 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( h `  i )  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  i
)  /\  dom  ( h `
 i )  e. 
om ) )
7669, 75sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  i )  e.  S  ->  ( (/) 
e.  dom  ( h `  i )  /\  dom  ( h `  i
)  e.  om )
)
7776simprd 450 . . . . . . . . . . . . . . . . . 18  |-  ( ( h `  i )  e.  S  ->  dom  ( h `  i
)  e.  om )
78 nnord 4845 . . . . . . . . . . . . . . . . . 18  |-  ( dom  ( h `  i
)  e.  om  ->  Ord 
dom  ( h `  i ) )
79 ordsucelsuc 4794 . . . . . . . . . . . . . . . . . 18  |-  ( Ord 
dom  ( h `  i )  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8077, 78, 793syl 19 . . . . . . . . . . . . . . . . 17  |-  ( ( h `  i )  e.  S  ->  (
i  e.  dom  (
h `  i )  <->  suc  i  e.  suc  dom  ( h `  i
) ) )
8180adantr 452 . . . . . . . . . . . . . . . 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 5062 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  ( h `  i )  ->  dom  x  =  dom  ( h `
 i ) )
83 suceq 4638 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2446 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  ( dom  y  =  suc  dom  x  <->  dom  y  =  suc  dom  ( h `  i
) ) )
8682reseq2d 5138 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  (
y  |`  dom  x )  =  ( y  |`  dom  ( h `  i
) ) )
87 id 20 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  ( h `  i )  ->  x  =  ( h `  i ) )
8886, 87eqeq12d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  =  ( h `  i )  ->  (
( y  |`  dom  x
)  =  x  <->  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) )
8985, 88anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . 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 2940 . . . . . . . . . . . . . . . . . . . . . 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 8322 . . . . . . . . . . . . . . . . . . . . . . 23  |-  S  e. 
_V
9493rabex 4346 . . . . . . . . . . . . . . . . . . . . . 22  |-  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i
)  /\  ( y  |` 
dom  ( h `  i ) )  =  ( h `  i
) ) }  e.  _V
9590, 91, 94fvmpt 5798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( h `  i )  e.  S  ->  ( G `  ( h `  i ) )  =  { y  e.  S  |  ( dom  y  =  suc  dom  ( h `  i )  /\  (
y  |`  dom  ( h `
 i ) )  =  ( h `  i ) ) } )
9695eleq2d 2502 . . . . . . . . . . . . . . . . . . . 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 5062 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  dom  y  =  dom  ( h `
 suc  i )
)
9897eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  ( dom  y  =  suc  dom  ( h `  i
)  <->  dom  ( h `  suc  i )  =  suc  dom  ( h `  i
) ) )
99 reseq1 5132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( h `  suc  i )  ->  (
y  |`  dom  ( h `
 i ) )  =  ( ( h `
 suc  i )  |` 
dom  ( h `  i ) ) )
10099eqeq1d 2443 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  =  ( h `  suc  i )  ->  (
( y  |`  dom  (
h `  i )
)  =  ( h `
 i )  <->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) ) )
10198, 100anbi12d 692 . . . . . . . . . . . . . . . . . . . . 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 3084 . . . . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . . . . 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 608 . . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . . 17  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  dom  ( h `
 suc  i )  =  suc  dom  ( h `  i ) )
106105eleq2d 2502 . . . . . . . . . . . . . . . 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 248 . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  i
)  e.  S  /\  ( h `  suc  i )  e.  ( G `  ( h `
 i ) ) )  ->  ( (
h `  suc  i )  |`  dom  ( h `  i ) )  =  ( h `  i
) )
110 resss 5162 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  i
)  |`  dom  ( h `
 i ) ) 
C_  ( h `  suc  i )
111 sseq1 3361 . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . 15  |-  ( ( ( h `  suc  i )  |`  dom  (
h `  i )
)  =  ( h `
 i )  -> 
( h `  i
)  C_  ( h `  suc  i ) )
113 elsuci 4639 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  suc  i  -> 
( j  e.  i  \/  j  =  i ) )
114 pm2.27 37 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  i  ->  (
( j  e.  i  ->  ( h `  j )  C_  (
h `  i )
)  ->  ( h `  j )  C_  (
h `  i )
) )
115 sstr2 3347 . . . . . . . . . . . . . . . . . . 19  |-  ( ( h `  j ) 
C_  ( h `  i )  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
116114, 115syl6 31 . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  (
h `  j )  =  ( h `  i ) )
118117sseq1d 3367 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
( h `  j
)  C_  ( h `  suc  i )  <->  ( h `  i )  C_  (
h `  suc  i ) ) )
119118biimprd 215 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  i  ->  (
( h `  i
)  C_  ( h `  suc  i )  -> 
( h `  j
)  C_  ( h `  suc  i ) ) )
120119a1d 23 . . . . . . . . . . . . . . . . . 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 369 . . . . . . . . . . . . . . . . 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 76 . . . . . . . . . . . . . . 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 19 . . . . . . . . . . . . . 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 547 . . . . . . . . . . . . 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 643 . . . . . . . . . . . 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 424 . . . . . . . . . . 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 4865 . . . . . . . . . 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 419 . . . . . . . . 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 450 . . . . . . . 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 425 . . . . . . 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 2787 . . . . . 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 2780 . . . . 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 5589 . . . . . . . . . . . 12  |-  ( h : om --> S  ->  ran  h  C_  S )
135 ffun 5585 . . . . . . . . . . . . . . . 16  |-  ( s : suc  n --> A  ->  Fun  s )
1361353ad2ant1 978 . . . . . . . . . . . . . . 15  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  Fun  s )
137136rexlimivw 2818 . . . . . . . . . . . . . 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 3407 . . . . . . . . . . . . 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 3370 . . . . . . . . . . . 12  |-  S  C_  { s  |  Fun  s }
140134, 139syl6ss 3352 . . . . . . . . . . 11  |-  ( h : om --> S  ->  ran  h  C_  { s  |  Fun  s } )
141140sseld 3339 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  u  e.  {
s  |  Fun  s } ) )
142 vex 2951 . . . . . . . . . . 11  |-  u  e. 
_V
143 funeq 5465 . . . . . . . . . . 11  |-  ( s  =  u  ->  ( Fun  s  <->  Fun  u ) )
144142, 143elab 3074 . . . . . . . . . 10  |-  ( u  e.  { s  |  Fun  s }  <->  Fun  u )
145141, 144syl6ib 218 . . . . . . . . 9  |-  ( h : om --> S  -> 
( u  e.  ran  h  ->  Fun  u )
)
146145adantr 452 . . . . . . . 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 5583 . . . . . . . . 9  |-  ( h : om --> S  ->  h  Fn  om )
148 fvelrnb 5766 . . . . . . . . . . . . 13  |-  ( h  Fn  om  ->  (
v  e.  ran  h  <->  E. b  e.  om  (
h `  b )  =  v ) )
149 fvelrnb 5766 . . . . . . . . . . . . . . 15  |-  ( h  Fn  om  ->  (
u  e.  ran  h  <->  E. a  e.  om  (
h `  a )  =  u ) )
150 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  e.  om  ->  Ord  a )
151 nnord 4845 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  om  ->  Ord  b )
152150, 151anim12i 550 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( a  e.  om  /\  b  e.  om )  ->  ( Ord  a  /\  Ord  b ) )
153 ordtri3or 4605 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Ord  a  /\  Ord  b )  ->  (
a  e.  b  \/  a  =  b  \/  b  e.  a ) )
154 fveq2 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  b  ->  (
h `  m )  =  ( h `  b ) )
155154sseq2d 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  b  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  b )
) )
156155raleqbi1dv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  b  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  b  ( h `  j )  C_  (
h `  b )
) )
157156rspcv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  a  ->  (
h `  j )  =  ( h `  a ) )
159158sseq1d 3367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  a  ->  (
( h `  j
)  C_  ( h `  b )  <->  ( h `  a )  C_  (
h `  b )
) )
160159rspccv 3041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  b  (
h `  j )  C_  ( h `  b
)  ->  ( a  e.  b  ->  ( h `
 a )  C_  ( h `  b
) ) )
161157, 160syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1147 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 382 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1152 . . . . . . . . . . . . . . . . . . . . . . . . 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 75 . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  b  ->  (
h `  a )  =  ( h `  b ) )
168 eqimss 3392 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( h `  a )  =  ( h `  b )  ->  (
h `  a )  C_  ( h `  b
) )
169168orcd 382 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( m  =  a  ->  (
h `  m )  =  ( h `  a ) )
174173sseq2d 3368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( m  =  a  ->  (
( h `  j
)  C_  ( h `  m )  <->  ( h `  j )  C_  (
h `  a )
) )
175174raleqbi1dv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( m  =  a  ->  ( A. j  e.  m  ( h `  j
)  C_  ( h `  m )  <->  A. j  e.  a  ( h `  j )  C_  (
h `  a )
) )
176175rspcv 3040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  b  ->  (
h `  j )  =  ( h `  b ) )
178177sseq1d 3367 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  b  ->  (
( h `  j
)  C_  ( h `  a )  <->  ( h `  b )  C_  (
h `  a )
) )
179178rspccv 3041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. j  e.  a  (
h `  j )  C_  ( h `  a
)  ->  ( b  e.  a  ->  ( h `
 b )  C_  ( h `  a
) ) )
180176, 179syl6 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1147 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 383 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1152 . . . . . . . . . . . . . . . . . . . . . . . . 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 75 . . . . . . . . . . . . . . . . . . . . . . . 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 1247 . . . . . . . . . . . . . . . . . . . . . . 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 34 . . . . . . . . . . . . . . . . . . . . 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 3363 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 a )  C_  ( h `  b
)  <->  u  C_  v ) )
190 sseq12 3363 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( h `  b
)  =  v  /\  ( h `  a
)  =  u )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
191190ancoms 440 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( h `
 b )  C_  ( h `  a
)  <->  v  C_  u
) )
192189, 191orbi12d 691 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( h `  a
)  =  u  /\  ( h `  b
)  =  v )  ->  ( ( ( h `  a ) 
C_  ( h `  b )  \/  (
h `  b )  C_  ( h `  a
) )  <->  ( u  C_  v  \/  v  C_  u ) ) )
193192biimpcd 216 . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . 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 74 . . . . . . . . . . . . . . . . . . 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 591 . . . . . . . . . . . . . . . . . 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 74 . . . . . . . . . . . . . . . . 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 2816 . . . . . . . . . . . . . . . 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 2821 . . . . . . . . . . . . . . 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 220 . . . . . . . . . . . . . 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 74 . . . . . . . . . . . . 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 207 . . . . . . . . . . . 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 83 . . . . . . . . . . 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 419 . . . . . . . . . 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 2787 . . . . . . . . 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 458 . . . . . . . 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 520 . . . . . . 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 2780 . . . . . 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 5509 . . . . . 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 457 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  Fun  U. ran  h )
212 vex 2951 . . . . . . . . 9  |-  m  e. 
_V
213212eldm2 5060 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u <. m ,  u >.  e.  U. ran  h )
214 eluni2 4011 . . . . . . . . . 10  |-  ( <.
m ,  u >.  e. 
U. ran  h  <->  E. v  e.  ran  h <. m ,  u >.  e.  v
)
215212, 142opeldm 5065 . . . . . . . . . . . . . . 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 3352 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) } )
218 ssel 3334 . . . . . . . . . . . . . . . 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 2951 . . . . . . . . . . . . . . . . . 18  |-  v  e. 
_V
220 dmeq 5062 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  v  ->  dom  s  =  dom  v )
221220eleq2d 2502 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  v ) )
222220eleq1d 2501 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  v  ->  ( dom  s  e.  om  <->  dom  v  e.  om )
)
223221, 222anbi12d 692 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  v  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) ) )
224219, 223elab 3074 . . . . . . . . . . . . . . . . 17  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  v  /\  dom  v  e. 
om ) )
225224simprbi 451 . . . . . . . . . . . . . . . 16  |-  ( v  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  ->  dom  v  e.  om )
226218, 225syl6 31 . . . . . . . . . . . . . . 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 547 . . . . . . . . . . . . 13  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  (
m  e.  dom  v  /\  dom  v  e.  om ) ) )
229 elnn 4847 . . . . . . . . . . . . 13  |-  ( ( m  e.  dom  v  /\  dom  v  e.  om )  ->  m  e.  om )
230228, 229syl6 31 . . . . . . . . . . . 12  |-  ( h : om --> S  -> 
( ( <. m ,  u >.  e.  v  /\  v  e.  ran  h )  ->  m  e.  om ) )
231230exp3acom23 1381 . . . . . . . . . . 11  |-  ( h : om --> S  -> 
( v  e.  ran  h  ->  ( <. m ,  u >.  e.  v  ->  m  e.  om )
) )
232231rexlimdv 2821 . . . . . . . . . 10  |-  ( h : om --> S  -> 
( E. v  e. 
ran  h <. m ,  u >.  e.  v  ->  m  e.  om )
)
233214, 232syl5bi 209 . . . . . . . . 9  |-  ( h : om --> S  -> 
( <. m ,  u >.  e.  U. ran  h  ->  m  e.  om )
)
234233exlimdv 1646 . . . . . . . 8  |-  ( h : om --> S  -> 
( E. u <. m ,  u >.  e.  U. ran  h  ->  m  e.  om ) )
235213, 234syl5bi 209 . . . . . . 7  |-  ( h : om --> S  -> 
( m  e.  dom  U.
ran  h  ->  m  e.  om ) )
236235adantr 452 . . . . . 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 446 . . . . . . . . 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 5859 . . . . . . . . . . . . 13  |-  ( ( h  Fn  om  /\  m  e.  om )  ->  ( h `  m
)  e.  ran  h
)
239 dmeq 5062 . . . . . . . . . . . . . . . 16  |-  ( u  =  ( h `  m )  ->  dom  u  =  dom  ( h `
 m ) )
240239eleq2d 2502 . . . . . . . . . . . . . . 15  |-  ( u  =  ( h `  m )  ->  (
m  e.  dom  u  <->  m  e.  dom  ( h `
 m ) ) )
241240rspcev 3044 . . . . . . . . . . . . . 14  |-  ( ( ( h `  m
)  e.  ran  h  /\  m  e.  dom  ( h `  m
) )  ->  E. u  e.  ran  h  m  e. 
dom  u )
242241ex 424 . . . . . . . . . . . . 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 458 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  m  e.  om )  ->  ( m  e.  dom  ( h `  m
)  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
245244ancoms 440 . . . . . . . . . 10  |-  ( ( m  e.  om  /\  h : om --> S )  ->  ( m  e. 
dom  ( h `  m )  ->  E. u  e.  ran  h  m  e. 
dom  u ) )
246245adantrr 698 . . . . . . . . 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 5071 . . . . . . . . . 10  |-  dom  U. ran  h  =  U_ u  e.  ran  h dom  u
249248eleq2i 2499 . . . . . . . . 9  |-  ( m  e.  dom  U. ran  h 
<->  m  e.  U_ u  e.  ran  h dom  u
)
250 eliun 4089 . . . . . . . . 9  |-  ( m  e.  U_ u  e. 
ran  h dom  u  <->  E. u  e.  ran  h  m  e.  dom  u )
251249, 250bitri 241 . . . . . . . 8  |-  ( m  e.  dom  U. ran  h 
<->  E. u  e.  ran  h  m  e.  dom  u )
252247, 251sylibr 204 . . . . . . 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 425 . . . . . 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 184 . . . . 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 2433 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  dom  U. ran  h  =  om )
256 rnuni 5275 . . . . . 6  |-  ran  U. ran  h  =  U_ s  e.  ran  h ran  s
257 frn 5589 . . . . . . . . . . . . . 14  |-  ( s : suc  n --> A  ->  ran  s  C_  A )
2582573ad2ant1 978 . . . . . . . . . . . . 13  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ran  s  C_  A )
259258rexlimivw 2818 . . . . . . . . . . . 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 3407 . . . . . . . . . . 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 3370 . . . . . . . . . 10  |-  S  C_  { s  |  ran  s  C_  A }
262134, 261syl6ss 3352 . . . . . . . . 9  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ran  s  C_  A } )
263 ssel 3334 . . . . . . . . . 10  |-  ( ran  h  C_  { s  |  ran  s  C_  A }  ->  ( s  e. 
ran  h  ->  s  e.  { s  |  ran  s  C_  A } ) )
264 abid 2423 . . . . . . . . . 10  |-  ( s  e.  { s  |  ran  s  C_  A } 
<->  ran  s  C_  A
)
265263, 264syl6ib 218 . . . . . . . . 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 2780 . . . . . . 7  |-  ( h : om --> S  ->  A. s  e.  ran  h ran  s  C_  A
)
268 iunss 4124 . . . . . . 7  |-  ( U_ s  e.  ran  h ran  s  C_  A  <->  A. s  e.  ran  h ran  s  C_  A )
269267, 268sylibr 204 . . . . . 6  |-  ( h : om --> S  ->  U_ s  e.  ran  h ran  s  C_  A
)
270256, 269syl5eqss 3384 . . . . 5  |-  ( h : om --> S  ->  ran  U. ran  h  C_  A )
271270adantr 452 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  ran  U. ran  h  C_  A )
272 df-fn 5449 . . . . 5  |-  ( U. ran  h  Fn  om  <->  ( Fun  U.
ran  h  /\  dom  U.
ran  h  =  om ) )
273 df-f 5450 . . . . . 6  |-  ( U. ran  h : om --> A  <->  ( U. ran  h  Fn  om  /\  ran  U. ran  h  C_  A ) )
274273biimpri 198 . . . . 5  |-  ( ( U. ran  h  Fn 
om  /\  ran  U. ran  h  C_  A )  ->  U. ran  h : om --> A )
275272, 274sylanbr 460 . . . 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 1183 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  U. ran  h : om --> A )
277 fnfvelrn 5859 . . . . . . . 8  |-  ( ( h  Fn  om  /\  (/) 
e.  om )  ->  (
h `  (/) )  e. 
ran  h )
278147, 25, 277sylancl 644 . . . . . . 7  |-  ( h : om --> S  -> 
( h `  (/) )  e. 
ran  h )
279278adantr 452 . . . . . 6  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( h `  (/) )  e. 
ran  h )
280 elssuni 4035 . . . . . 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 452 . . . . 5  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  (/) 
e.  dom  ( h `  (/) ) )
283 funssfv 5738 . . . . 5  |-  ( ( Fun  U. ran  h  /\  ( h `  (/) )  C_  U.
ran  h  /\  (/)  e.  dom  ( h `  (/) ) )  ->  ( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
284211, 281, 282, 283syl3anc 1184 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
285 simp2 958 . . . . . . . . . . 11  |-  ( ( s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) )  ->  ( s `  (/) )  =  C )
286285rexlimivw 2818 . . . . . . . . . 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 3407 . . . . . . . . 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 3370 . . . . . . . 8  |-  S  C_  { s  |  ( s `
 (/) )  =  C }
289134, 288syl6ss 3352 . . . . . . 7  |-  ( h : om --> S  ->  ran  h  C_  { s  |  ( s `  (/) )  =  C }
)
290 ssel 3334 . . . . . . . 8  |-  ( ran  h  C_  { s  |  ( s `  (/) )  =  C }  ->  ( ( h `  (/) )  e.  ran  h  ->  ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C } ) )
291 fveq1 5719 . . . . . . . . . 10  |-  ( s  =  ( h `  (/) )  ->  ( s `  (/) )  =  ( ( h `  (/) ) `  (/) ) )
292291eqeq1d 2443 . . . . . . . . 9  |-  ( s  =  ( h `  (/) )  ->  ( (
s `  (/) )  =  C  <->  ( ( h `
 (/) ) `  (/) )  =  C ) )
29346, 292elab 3074 . . . . . . . 8  |-  ( ( h `  (/) )  e. 
{ s  |  ( s `  (/) )  =  C }  <->  ( (
h `  (/) ) `  (/) )  =  C )
294290, 293syl6ib 218 . . . . . . 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 452 . . . . 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 2467 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( U. ran  h `  (/) )  =  C )
299 nfv 1629 . . . . 5  |-  F/ k  h : om --> S
300 nfra1 2748 . . . . 5  |-  F/ k A. k  e.  om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) )
301299, 300nfan 1846 . . . 4  |-  F/ k ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )
302134ad2antrr 707 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ran  h  C_  S )
303 peano2 4857 . . . . . . . . 9  |-  ( k  e.  om  ->  suc  k  e.  om )
304 fnfvelrn 5859 . . . . . . . . 9  |-  ( ( h  Fn  om  /\  suc  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
305147, 303, 304syl2an 464 . . . . . . . 8  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( h `  suc  k )  e.  ran  h )
306305adantlr 696 . . . . . . 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 425 . . . . . . . . 9  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( m  e.  om  ->  m  e.  dom  (
h `  m )
) )
308307ralrimiv 2780 . . . . . . . 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 20 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  m  =  suc  k )
310 fveq2 5720 . . . . . . . . . . . 12  |-  ( m  =  suc  k  -> 
( h `  m
)  =  ( h `
 suc  k )
)
311310dmeqd 5064 . . . . . . . . . . 11  |-  ( m  =  suc  k  ->  dom  ( h `  m
)  =  dom  (
h `  suc  k ) )
312309, 311eleq12d 2503 . . . . . . . . . 10  |-  ( m  =  suc  k  -> 
( m  e.  dom  ( h `  m
)  <->  suc  k  e.  dom  ( h `  suc  k ) ) )
313312rspcv 3040 . . . . . . . . 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 456 . . . . . . 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 2496 . . . . . . . . . . . . . . . . . . . . 21  |-  ( dom  s  =  suc  n  ->  ( suc  k  e. 
dom  s  <->  suc  k  e. 
suc  n ) )
317316biimpa 471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( dom  s  =  suc  n  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
31829, 317sylan 458 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s : suc  n --> A  /\  suc  k  e. 
dom  s )  ->  suc  k  e.  suc  n )
319 ordsucelsuc 4794 . . . . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  e.  om  ->  ( suc  k  e.  suc  n  ->  k  e.  n
) )
322 rsp 2758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. k  e.  n  (
s `  suc  k )  e.  ( F `  ( s `  k
) )  ->  (
k  e.  n  -> 
( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) )
323321, 322syl9r 69 . . . . . . . . . . . . . . . . . . . 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 76 . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . 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 83 . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . 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 2817 . . . . . . . . . . . 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 3407 . . . . . . . . . . 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 3370 . . . . . . . . . 10  |-  S  C_  { s  |  ( suc  k  e.  dom  s  ->  ( s `  suc  k )  e.  ( F `  ( s `
 k ) ) ) }
334 sstr 3348 . . . . . . . . . 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 653 . . . . . . . . 9  |-  ( ran  h  C_  S  ->  ran  h  C_  { s  |  ( suc  k  e.  dom  s  ->  (
s `  suc  k )  e.  ( F `  ( s `  k
) ) ) } )
336335sseld 3339 . . . . . . . 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 5734 . . . . . . . . 9  |-  ( h `
 suc  k )  e.  _V
338 dmeq 5062 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  dom  s  =  dom  ( h `
 suc  k )
)
339338eleq2d 2502 . . . . . . . . . 10  |-  ( s  =  ( h `  suc  k )  ->  ( suc  k  e.  dom  s 
<->  suc  k  e.  dom  ( h `  suc  k ) ) )
340 fveq1 5719 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  (
s `  suc  k )  =  ( ( h `
 suc  k ) `  suc  k ) )
341 fveq1 5719 . . . . . . . . . . . 12  |-  ( s  =  ( h `  suc  k )  ->  (
s `  k )  =  ( ( h `
 suc  k ) `  k ) )
342341fveq2d 5724 . . . . . . . . . . 11  |-  ( s  =  ( h `  suc  k )  ->  ( F `  ( s `  k ) )  =  ( F `  (
( h `  suc  k ) `  k
) ) )
343340, 342eleq12d 2503 . . . . . . . . . 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 312 . . . . . . . . 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 3074 . . . . . . . 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 218 . . . . . . 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 59 . . . . . 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 452 . . . . . . . 8  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  Fun  U.
ran  h )
349 elssuni 4035 . . . . . . . . . 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 696 . . . . . . . 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 5738 . . . . . . . 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 1184 . . . . . . 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 3339 . . . . . . . . . . . . . . . 16  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( h `  suc  k )  e.  {
s  |  ( (/)  e.  dom  s  /\  dom  s  e.  om ) } ) )
355338eleq2d 2502 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  suc  k )  ->  ( (/) 
e.  dom  s  <->  (/)  e.  dom  ( h `  suc  k ) ) )
356338eleq1d 2501 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  ( h `  suc  k )  ->  ( dom  s  e.  om  <->  dom  ( h `  suc  k )  e.  om ) )
357355, 356anbi12d 692 . . . . . . . . . . . . . . . . 17  |-  ( s  =  ( h `  suc  k )  ->  (
( (/)  e.  dom  s  /\  dom  s  e.  om ) 
<->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
358337, 357elab 3074 . . . . . . . . . . . . . . . 16  |-  ( ( h `  suc  k
)  e.  { s  |  ( (/)  e.  dom  s  /\  dom  s  e. 
om ) }  <->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
359354, 358syl6ib 218 . . . . . . . . . . . . . . 15  |-  ( h : om --> S  -> 
( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
360359adantr 452 . . . . . . . . . . . . . 14  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( ( h `  suc  k )  e.  ran  h  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) ) )
361305, 360mpd 15 . . . . . . . . . . . . 13  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( (/)  e.  dom  ( h `  suc  k )  /\  dom  ( h `  suc  k )  e.  om ) )
362361simprd 450 . . . . . . . . . . . 12  |-  ( ( h : om --> S  /\  k  e.  om )  ->  dom  ( h `  suc  k )  e.  om )
363 nnord 4845 . . . . . . . . . . . 12  |-  ( dom  ( h `  suc  k )  e.  om  ->  Ord  dom  ( h `  suc  k ) )
364362, 363syl 16 . . . . . . . . . . 11  |-  ( ( h : om --> S  /\  k  e.  om )  ->  Ord  dom  ( h `  suc  k ) )
365 ordtr 4587 . . . . . . . . . . 11  |-  ( Ord 
dom  ( h `  suc  k )  ->  Tr  dom  ( h `  suc  k ) )
366 trsuc 4658 . . . . . . . . . . . 12  |-  ( ( Tr  dom  ( h `
 suc  k )  /\  suc  k  e.  dom  ( h `  suc  k ) )  -> 
k  e.  dom  (
h `  suc  k ) )
367366ex 424 . . . . . . . . . . 11  |-  ( Tr 
dom  ( h `  suc  k )  ->  ( suc  k  e.  dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
368364, 365, 3673syl 19 . . . . . . . . . 10  |-  ( ( h : om --> S  /\  k  e.  om )  ->  ( suc  k  e. 
dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
369368adantlr 696 . . . . . . . . 9  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ( suc  k  e.  dom  ( h `  suc  k )  ->  k  e.  dom  ( h `  suc  k ) ) )
370315, 369mpd 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 ) )
371 funssfv 5738 . . . . . . . 8  |-  ( ( Fun  U. ran  h  /\  ( h `  suc  k )  C_  U. ran  h  /\  k  e.  dom  ( h `  suc  k ) )  -> 
( U. ran  h `  k )  =  ( ( h `  suc  k ) `  k
) )
372348, 351, 370, 371syl3anc 1184 . . . . . . 7  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ( U. ran  h `  k
)  =  ( ( h `  suc  k
) `  k )
)
373 simpl 444 . . . . . . . 8  |-  ( ( ( U. ran  h `  suc  k )  =  ( ( h `  suc  k ) `  suc  k )  /\  ( U. ran  h `  k
)  =  ( ( h `  suc  k
) `  k )
)  ->  ( U. ran  h `  suc  k
)  =  ( ( h `  suc  k
) `  suc  k ) )
374 simpr 448 . . . . . . . . 9  |-  ( ( ( U. ran  h `  suc  k )  =  ( ( h `  suc  k ) `  suc  k )  /\  ( U. ran  h `  k
)  =  ( ( h `  suc  k
) `  k )
)  ->  ( U. ran  h `  k )  =  ( ( h `
 suc  k ) `  k ) )
375374fveq2d 5724 . . . . . . . 8  |-  ( ( ( U. ran  h `  suc  k )  =  ( ( h `  suc  k ) `  suc  k )  /\  ( U. ran  h `  k
)  =  ( ( h `  suc  k
) `  k )
)  ->  ( F `  ( U. ran  h `  k ) )  =  ( F `  (
( h `  suc  k ) `  k
) ) )
376373, 375eleq12d 2503 . . . . . . 7  |-  ( ( ( U. ran  h `  suc  k )  =  ( ( h `  suc  k ) `  suc  k )  /\  ( U. ran  h `  k
)  =  ( ( h `  suc  k
) `  k )
)  ->  ( ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) )  <->  ( ( h `
 suc  k ) `  suc  k )  e.  ( F `  (
( h `  suc  k ) `  k
) ) ) )
377353, 372, 376syl2anc 643 . . . . . 6  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  (
( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) )  <->  ( (
h `  suc  k ) `
 suc  k )  e.  ( F `  (
( h `  suc  k ) `  k
) ) ) )
378347, 377mpbird 224 . . . . 5  |-  ( ( ( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) )  /\  k  e. 
om )  ->  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) ) )
379378ex 424 . . . 4  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  -> 
( k  e.  om  ->  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) ) ) )
380301, 379ralrimi 2779 . . 3  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  A. k  e.  om  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) ) )
381 vex 2951 . . . . . 6  |-  h  e. 
_V
382381rnex 5125 . . . . 5  |-  ran  h  e.  _V
383382uniex 4697 . . . 4  |-  U. ran  h  e.  _V
384 feq1 5568 . . . . 5  |-  ( g  =  U. ran  h  ->  ( g : om --> A 
<-> 
U. ran  h : om
--> A ) )
385 fveq1 5719 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( g `  (/) )  =  ( U. ran  h `  (/) ) )
386385eqeq1d 2443 . . . . 5  |-  ( g  =  U. ran  h  ->  ( ( g `  (/) )  =  C  <->  ( U. ran  h `  (/) )  =  C ) )
387 fveq1 5719 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( g `  suc  k )  =  ( U. ran  h `  suc  k ) )
388 fveq1 5719 . . . . . . . 8  |-  ( g  =  U. ran  h  ->  ( g `  k
)  =  ( U. ran  h `  k ) )
389388fveq2d 5724 . . . . . . 7  |-  ( g  =  U. ran  h  ->  ( F `  (
g `  k )
)  =  ( F `
 ( U. ran  h `  k )
) )
390387, 389eleq12d 2503 . . . . . 6  |-  ( g  =  U. ran  h  ->  ( ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k
) ) ) )
391390ralbidv 2717 . . . . 5  |-  ( g  =  U. ran  h  ->  ( A. k  e. 
om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <->  A. k  e.  om  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) ) ) )
392384, 386, 3913anbi123d 1254 . . . 4  |-  ( g  =  U. ran  h  ->  ( ( g : om --> A  /\  (
g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) )  <->  ( U. ran  h : om --> A  /\  ( U. ran  h `  (/) )  =  C  /\  A. k  e.  om  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) ) ) ) )
393383, 392spcev 3035 . . 3  |-  ( ( U. ran  h : om --> A  /\  ( U. ran  h `  (/) )  =  C  /\  A. k  e.  om  ( U. ran  h `  suc  k )  e.  ( F `  ( U. ran  h `  k ) ) )  ->  E. g ( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) )
394276, 298, 380, 393syl3anc 1184 . 2  |-  ( ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  E. g ( g : om --> A  /\  (
g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) )
395394exlimiv 1644 1  |-  ( E. h ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) )  ->  E. g ( g : om --> A  /\  (
g `  (/) )  =  C  /\  A. k  e.  om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    \/ w3o 935    /\ w3a 936   E.wex 1550    = wceq 1652    e. wcel 1725   {cab 2421   A.wral 2697   E.wrex 2698   {crab 2701   _Vcvv 2948    C_ wss 3312   (/)c0 3620   <.cop 3809   U.cuni 4007   U_ciun 4085    e. cmpt 4258   Tr wtr 4294   Ord word 4572   suc csuc 4575   omcom 4837   dom cdm 4870   ran crn 4871    |` cres 4872   Fun wfun 5440    Fn wfn 5441   -->wf 5442   ` cfv 5446
This theorem is referenced by:  axdc3lem4  8325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-dc 8318
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-fv 5454  df-1o 6716
  Copyright terms: Public domain W3C validator