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

Theorem axdc3lem4 8834
Description: Lemma for axdc3 8835. 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 8827 (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 8827 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  S is nonempty, and that  G always maps to a nonempty subset of  S, so that we can apply axdc2 8830. See axdc3lem2 8832 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013.)
Hypotheses
Ref Expression
axdc3lem4.1  |-  A  e. 
_V
axdc3lem4.2  |-  S  =  { s  |  E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) ) }
axdc3lem4.3  |-  G  =  ( x  e.  S  |->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) } )
Assertion
Ref Expression
axdc3lem4  |-  ( ( C  e.  A  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. g
( g : om --> A  /\  ( g `  (/) )  =  C  /\  A. k  e.  om  (
g `  suc  k )  e.  ( F `  ( g `  k
) ) ) )
Distinct variable groups:    A, g,
k    A, n, x, k, s    C, g, k    C, n, s    g, F, k   
n, F, x, s   
k, G    S, k,
s, x    y, S, x    n, s
Allowed substitution hints:    A( y)    C( x, y)    S( g, n)    F( y)    G( x, y, g, n, s)

Proof of Theorem axdc3lem4
Dummy variables  h  m  p  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano1 6670 . . . . . 6  |-  (/)  e.  om
2 eqid 2428 . . . . . . . . . 10  |-  { <. (/)
,  C >. }  =  { <. (/) ,  C >. }
3 fsng 6022 . . . . . . . . . . 11  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
41, 3mpan 674 . . . . . . . . . 10  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
52, 4mpbiri 236 . . . . . . . . 9  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> { C } )
6 snssi 4087 . . . . . . . . 9  |-  ( C  e.  A  ->  { C }  C_  A )
75, 6fssd 5698 . . . . . . . 8  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> A )
8 suc0 5459 . . . . . . . . 9  |-  suc  (/)  =  { (/)
}
98feq2i 5682 . . . . . . . 8  |-  ( {
<. (/) ,  C >. } : suc  (/) --> A  <->  { <. (/) ,  C >. } : { (/) } --> A )
107, 9sylibr 215 . . . . . . 7  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : suc  (/) --> A )
11 fvsng 6057 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
121, 11mpan 674 . . . . . . 7  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
13 ral0 3847 . . . . . . . 8  |-  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) )
1413a1i 11 . . . . . . 7  |-  ( C  e.  A  ->  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) )
1510, 12, 143jca 1185 . . . . . 6  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )
16 suceq 5450 . . . . . . . . 9  |-  ( m  =  (/)  ->  suc  m  =  suc  (/) )
1716feq2d 5676 . . . . . . . 8  |-  ( m  =  (/)  ->  ( {
<. (/) ,  C >. } : suc  m --> A  <->  { <. (/) ,  C >. } : suc  (/) --> A ) )
18 raleq 2964 . . . . . . . 8  |-  ( m  =  (/)  ->  ( A. k  e.  m  ( { <. (/) ,  C >. } `
 suc  k )  e.  ( F `  ( { <. (/) ,  C >. } `
 k ) )  <->  A. k  e.  (/)  ( {
<. (/) ,  C >. } `
 suc  k )  e.  ( F `  ( { <. (/) ,  C >. } `
 k ) ) ) )
1917, 183anbi13d 1337 . . . . . . 7  |-  ( m  =  (/)  ->  ( ( { <. (/) ,  C >. } : suc  m --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  m  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) )  <->  ( { <. (/)
,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) ) )
2019rspcev 3125 . . . . . 6  |-  ( (
(/)  e.  om  /\  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )  ->  E. m  e.  om  ( { <. (/)
,  C >. } : suc  m --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  m  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) ) )
211, 15, 20sylancr 667 . . . . 5  |-  ( C  e.  A  ->  E. m  e.  om  ( { <. (/)
,  C >. } : suc  m --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  m  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) ) )
22 axdc3lem4.1 . . . . . 6  |-  A  e. 
_V
23 axdc3lem4.2 . . . . . 6  |-  S  =  { s  |  E. n  e.  om  (
s : suc  n --> A  /\  ( s `  (/) )  =  C  /\  A. k  e.  n  ( s `  suc  k
)  e.  ( F `
 ( s `  k ) ) ) }
24 snex 4605 . . . . . 6  |-  { <. (/)
,  C >. }  e.  _V
2522, 23, 24axdc3lem3 8833 . . . . 5  |-  ( {
<. (/) ,  C >. }  e.  S  <->  E. m  e.  om  ( { <. (/)
,  C >. } : suc  m --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  m  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) ) )
2621, 25sylibr 215 . . . 4  |-  ( C  e.  A  ->  { <. (/)
,  C >. }  e.  S )
27 ne0i 3710 . . . 4  |-  ( {
<. (/) ,  C >. }  e.  S  ->  S  =/=  (/) )
2826, 27syl 17 . . 3  |-  ( C  e.  A  ->  S  =/=  (/) )
29 ssrab2 3489 . . . . . . 7  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S
3022, 23axdc3lem 8831 . . . . . . . 8  |-  S  e. 
_V
3130elpw2 4531 . . . . . . 7  |-  ( { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  ~P S  <->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S )
3229, 31mpbir 212 . . . . . 6  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ~P S
3332a1i 11 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ~P S )
34 vex 3025 . . . . . . . . . 10  |-  x  e. 
_V
3522, 23, 34axdc3lem3 8833 . . . . . . . . 9  |-  ( x  e.  S  <->  E. m  e.  om  ( x : suc  m --> A  /\  ( x `  (/) )  =  C  /\  A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
) ) )
36 simp2 1006 . . . . . . . . . . . . . . . 16  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  x : suc  m --> A )
37 vex 3025 . . . . . . . . . . . . . . . . . . . . . 22  |-  m  e. 
_V
3837sucid 5464 . . . . . . . . . . . . . . . . . . . . 21  |-  m  e. 
suc  m
39 ffvelrn 5979 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x : suc  m --> A  /\  m  e.  suc  m )  ->  (
x `  m )  e.  A )
4038, 39mpan2 675 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : suc  m --> A  -> 
( x `  m
)  e.  A )
41 ffvelrn 5979 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( x `
 m )  e.  A )  ->  ( F `  ( x `  m ) )  e.  ( ~P A  \  { (/) } ) )
4240, 41sylan2 476 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( F `  ( x `  m
) )  e.  ( ~P A  \  { (/)
} ) )
43 eldifn 3531 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  -.  ( F `  (
x `  m )
)  e.  { (/) } )
44 fvex 5835 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( x `  m ) )  e. 
_V
4544elsnc 3965 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( x `
 m ) )  e.  { (/) }  <->  ( F `  ( x `  m
) )  =  (/) )
4645necon3bbii 2648 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <-> 
( F `  (
x `  m )
)  =/=  (/) )
47 n0 3714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  ( x `
 m ) )  =/=  (/)  <->  E. z  z  e.  ( F `  (
x `  m )
) )
4846, 47bitri 252 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <->  E. z  z  e.  ( F `  ( x `
 m ) ) )
4943, 48sylib 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5042, 49syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  E. z  z  e.  ( F `  (
x `  m )
) )
51 simp32 1042 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
)  ->  x : suc  m --> A )
52 eldifi 3530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  -> 
( F `  (
x `  m )
)  e.  ~P A
)
53 elelpwi 3935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( F `  ( x `
 m ) )  e.  ~P A )  ->  z  e.  A
)
5453expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ~P A  -> 
( z  e.  ( F `  ( x `
 m ) )  ->  z  e.  A
) )
5542, 52, 543syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  z  e.  A ) )
56 peano2 6671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  om  ->  suc  m  e.  om )
57563ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  suc  m  e.  om )
58573ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  ->  suc  m  e.  om )
59 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  x : suc  m --> A )
6034dmex 6684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  dom  x  e.  _V
61 vex 3025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  z  e. 
_V
62 eqid 2428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  { <. dom  x ,  z >. }  =  { <. dom  x ,  z >. }
63 fsng 6022 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  ( { <. dom  x ,  z >. } : { dom  x } --> { z }  <->  { <. dom  x , 
z >. }  =  { <. dom  x ,  z
>. } ) )
6462, 63mpbiri 236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  { <. dom  x , 
z >. } : { dom  x } --> { z } )
6560, 61, 64mp2an 676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  { <. dom  x ,  z >. } : { dom  x }
--> { z }
66 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  z  e.  A )
6766snssd 4088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { z }  C_  A )
68 fss 5697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( { <. dom  x , 
z >. } : { dom  x } --> { z }  /\  { z }  C_  A )  ->  { <. dom  x , 
z >. } : { dom  x } --> A )
6965, 67, 68sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { <. dom  x ,  z >. } : { dom  x }
--> A )
70 fdm 5693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  dom  x  =  suc  m
)
7156adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  suc  m  e. 
om )
72 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
om 
<->  suc  m  e.  om ) )
7372adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  om  <->  suc  m  e. 
om ) )
7471, 73mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  dom  x  e. 
om )
75 nnord 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  e.  om  ->  Ord 
dom  x )
76 ordirr 5403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( Ord 
dom  x  ->  -.  dom  x  e.  dom  x
)
7774, 75, 763syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  dom  x )
78 eleq2 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
dom  x  <->  dom  x  e. 
suc  m ) )
7978adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  dom  x  <->  dom  x  e. 
suc  m ) )
8077, 79mtbid 301 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  suc  m )
81 disjsn 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( suc  m  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
suc  m )
8280, 81sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
8370, 82sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( suc  m  i^i  { dom  x }
)  =  (/) )
8483adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
85 fun2 5707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( x : suc  m
--> A  /\  { <. dom  x ,  z >. } : { dom  x }
--> A )  /\  ( suc  m  i^i  { dom  x } )  =  (/) )  ->  ( x  u. 
{ <. dom  x , 
z >. } ) : ( suc  m  u. 
{ dom  x }
) --> A )
8659, 69, 84, 85syl21anc 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : ( suc  m  u.  { dom  x } ) --> A )
87 sneq 3951 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( dom  x  =  suc  m  ->  { dom  x }  =  { suc  m }
)
8887uneq2d 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  ( suc  m  u.  { suc  m } ) )
89 df-suc 5391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  suc  suc  m  =  ( suc  m  u.  { suc  m } )
9088, 89syl6eqr 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  suc  suc  m )
9170, 90syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( suc  m  u.  { dom  x } )  =  suc  suc  m
)
9291ad2antlr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  u.  { dom  x } )  =  suc  suc  m )
9392feq2d 5676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) : ( suc  m  u.  { dom  x } ) --> A  <-> 
( x  u.  { <. dom  x ,  z
>. } ) : suc  suc  m --> A ) )
9486, 93mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A )
9594ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  A  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
9695adantrd 469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( z  e.  A  /\  (
x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) )
9796a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
z  e.  A  /\  ( x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) ) )
9897ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
z  e.  A  /\  ( x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) ) )
99983adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
z  e.  ( F `
 ( x `  m ) )  -> 
( ( z  e.  A  /\  ( x `
 (/) )  =  C )  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) ) )
100993imp 1199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  -> 
( x  u.  { <. dom  x ,  z
>. } ) : suc  suc  m --> A )
101 ffun 5691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  Fun  x )
102101adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  x )
10360, 61funsn 5592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  Fun  { <. dom  x ,  z
>. }
104102, 103jctir 540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( Fun  x  /\  Fun  { <. dom  x ,  z >. } ) )
10561dmsnop 5272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  dom  { <. dom  x ,  z
>. }  =  { dom  x }
106105ineq2i 3604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  i^i  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  i^i  { dom  x } )
107 disjsn 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
dom  x )
10877, 107sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  { dom  x } )  =  (/) )
109106, 108syl5eq 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
11070, 109sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
111 funun 5586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( Fun  x  /\  Fun  { <. dom  x , 
z >. } )  /\  ( dom  x  i^i  dom  {
<. dom  x ,  z
>. } )  =  (/) )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
112104, 110, 111syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
113 ssun1 3572 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  x  C_  ( x  u.  { <. dom  x ,  z >. } )
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
115 nnord 6658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  om  ->  Ord  m )
116 0elsuc 6620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( Ord  m  ->  (/)  e.  suc  m )
117115, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  om  ->  (/)  e.  suc  m )
118117adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  suc  m
)
11970eleq2d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( (/)  e.  dom  x  <->  (/)  e.  suc  m ) )
120119adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( (/)  e.  dom  x 
<->  (/)  e.  suc  m ) )
121118, 120mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  dom  x
)
122 funssfv 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( Fun  ( x  u. 
{ <. dom  x , 
z >. } )  /\  x  C_  ( x  u. 
{ <. dom  x , 
z >. } )  /\  (/) 
e.  dom  x )  ->  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  ( x `
 (/) ) )
123112, 114, 121, 122syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 (/) )  =  ( x `  (/) ) )
124123eqeq1d 2430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
125124ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
1261253adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
127126biimpar 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  (
x `  (/) )  =  C )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  (/) )  =  C )
128127adantrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  (
z  e.  A  /\  ( x `  (/) )  =  C ) )  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C )
1291283adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C )
130 nfra1 2746 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )
131 nfv 1755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  x : suc  m --> A
132 nfv 1755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  m  e.  om
133130, 131, 132nf3an 1990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )
134 nfv 1755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k  z  e.  ( F `
 ( x `  m ) )
135 nfv 1755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( z  e.  A  /\  ( x `  (/) )  =  C )
136133, 134, 135nf3an 1990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/ k ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )
137 simplr 760 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  k  e.  suc  m )
138 elsuci 5451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  suc  m  -> 
( k  e.  m  \/  k  =  m
) )
139 rsp 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
k  e.  m  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) ) )
140139impcom 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( k  e.  m  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
141140ad2ant2lr 752 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m ) )  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
1421413adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
143112adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  Fun  ( x  u.  { <. dom  x ,  z >. } ) )
144113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  x  C_  ( x  u.  { <. dom  x ,  z
>. } ) )
145 ordsucelsuc 6607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( Ord  m  ->  ( k  e.  m  <->  suc  k  e.  suc  m ) )
146115, 145syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( m  e.  om  ->  (
k  e.  m  <->  suc  k  e. 
suc  m ) )
147146biimpa 486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  m )  ->  suc  k  e.  suc  m )
148 eleq2 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  m  ->  ( suc  k  e. 
dom  x  <->  suc  k  e. 
suc  m ) )
149148biimparc 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( suc  k  e.  suc  m  /\  dom  x  =  suc  m )  ->  suc  k  e.  dom  x )
150147, 70, 149syl2an 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  suc  k  e.  dom  x )
151 funssfv 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( Fun  ( x  u. 
{ <. dom  x , 
z >. } )  /\  x  C_  ( x  u. 
{ <. dom  x , 
z >. } )  /\  suc  k  e.  dom  x )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
152143, 144, 150, 151syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1531523adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1541123adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
155113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
156 eleq2 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( dom  x  =  suc  m  ->  ( k  e.  dom  x 
<->  k  e.  suc  m
) )
157156biimparc 489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  e.  suc  m  /\  dom  x  =  suc  m )  ->  k  e.  dom  x )
15870, 157sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
1591583adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
160 funssfv 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( Fun  ( x  u. 
{ <. dom  x , 
z >. } )  /\  x  C_  ( x  u. 
{ <. dom  x , 
z >. } )  /\  k  e.  dom  x )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
161154, 155, 159, 160syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
1621613adant1r 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
163162fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  ( F `  ( (
x  u.  { <. dom  x ,  z >. } ) `  k
) )  =  ( F `  ( x `
 k ) ) )
164153, 163eleq12d 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) )  <->  ( x `  suc  k )  e.  ( F `  (
x `  k )
) ) )
1651643adant2l 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) )  <->  ( x `  suc  k )  e.  ( F `  (
x `  k )
) ) )
166142, 165mpbird 235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) ) )
167166a1d 26 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
1681673expib 1208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  k  e.  m )  ->  ( ( ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) )
169168expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( k  e.  m  ->  (
m  e.  om  ->  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
1701123adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
171 ssun2 3573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  { <. dom  x ,  z >. }  C_  ( x  u. 
{ <. dom  x , 
z >. } )
172171a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  { <. dom  x ,  z >. }  C_  ( x  u.  { <. dom  x ,  z >. } ) )
173 suceq 5450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( k  =  m  ->  suc  k  =  suc  m )
174173eqeq2d 2438 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( k  =  m  ->  ( dom  x  =  suc  k  <->  dom  x  =  suc  m
) )
175174biimpar 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  dom  x  =  suc  k )
17660snid 3969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  dom  x  e.  { dom  x }
177176, 105eleqtrri 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  dom  x  e.  dom  { <. dom  x ,  z >. }
178175, 177syl6eqelr 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  suc  k  e. 
dom  { <. dom  x , 
z >. } )
17970, 178sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
1801793adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
181 funssfv 5840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( Fun  ( x  u. 
{ <. dom  x , 
z >. } )  /\  {
<. dom  x ,  z
>. }  C_  ( x  u.  { <. dom  x , 
z >. } )  /\  suc  k  e.  dom  {
<. dom  x ,  z
>. } )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
182170, 172, 180, 181syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  ( { <. dom  x ,  z >. } `  suc  k ) )
1831753adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  dom  x  =  suc  k )
18460, 61fvsn 6056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( {
<. dom  x ,  z
>. } `  dom  x
)  =  z
185 fveq2 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  dom  x )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
186184, 185syl5reqr 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
187183, 186syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
18870, 187syl3an3 1299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
189182, 188eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  z )
1901893expa 1205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1911903adant2 1024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1921613adant1l 1256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
193 fveq2 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( k  =  m  ->  (
x `  k )  =  ( x `  m ) )
194193adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( x `  k
)  =  ( x `
 m ) )
1951943ad2ant1 1026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
x `  k )  =  ( x `  m ) )
196192, 195eqtrd 2462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 m ) )
197196fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  ( F `  ( (
x  u.  { <. dom  x ,  z >. } ) `  k
) )  =  ( F `  ( x `
 m ) ) )
198191, 197eleq12d 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) )  <->  z  e.  ( F `  ( x `
 m ) ) ) )
1991983adant2l 1258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) )  <->  z  e.  ( F `  ( x `
 m ) ) ) )
200199biimprd 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
2012003expib 1208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( ( ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) )
202201ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( k  =  m  ->  (
m  e.  om  ->  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
203169, 202jaoi 380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( k  e.  m  \/  k  =  m )  ->  ( m  e. 
om  ->  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
204138, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( k  e.  suc  m  -> 
( m  e.  om  ->  ( ( ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
205204com3r 82 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( k  e. 
suc  m  ->  (
m  e.  om  ->  ( z  e.  ( F `
 ( x `  m ) )  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
206137, 205mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  ( m  e. 
om  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) )
207206ex 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  ->  (
x : suc  m --> A  ->  ( m  e. 
om  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) ) )
208207expcom 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  suc  m  -> 
( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  ->  ( x : suc  m --> A  -> 
( m  e.  om  ->  ( z  e.  ( F `  ( x `
 m ) )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) ) ) ) ) ) )
2092083impd 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  suc  m  -> 
( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om )  ->  (
z  e.  ( F `
 ( x `  m ) )  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) )
210209impd 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( k  e.  suc  m  -> 
( ( ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )  /\  z  e.  ( F `  ( x `  m ) ) )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) ) ) )
211210com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
) )  ->  (
k  e.  suc  m  ->  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
2122113adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  -> 
( k  e.  suc  m  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) ) ) )
213136, 212ralrimi 2765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  ->  A. k  e.  suc  m ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) ) )
214 suceq 5450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( p  =  suc  m  ->  suc  p  =  suc  suc  m )
215214feq2d 5676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  <->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
216 raleq 2964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( A. k  e.  p  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  e.  ( F `  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
) )  <->  A. k  e.  suc  m ( ( x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
217215, 2163anbi13d 1337 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( p  =  suc  m  -> 
( ( ( x  u.  { <. dom  x ,  z >. } ) : suc  p --> A  /\  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C  /\  A. k  e.  p  ( ( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) )  <->  ( (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A  /\  (
( x  u.  { <. dom  x ,  z
>. } ) `  (/) )  =  C  /\  A. k  e.  suc  m ( ( x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) ) )
218217rspcev 3125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( suc  m  e.  om  /\  ( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  suc  m --> A  /\  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C  /\  A. k  e.  suc  m
( ( x  u. 
{ <. dom  x , 
z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )  ->  E. p  e.  om  ( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  /\  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C  /\  A. k  e.  p  ( ( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
21958, 100, 129, 213, 218syl13anc 1266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  ->  E. p  e.  om  ( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  /\  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  C  /\  A. k  e.  p  ( ( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
220 snex 4605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  e.  _V
22134, 220unex 6547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  u.  { <. dom  x ,  z >. } )  e.  _V
22222, 23, 221axdc3lem3 8833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( x  u.  { <. dom  x ,  z >. } )  e.  S  <->  E. p  e.  om  (
( x  u.  { <. dom  x ,  z
>. } ) : suc  p
--> A  /\  ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  /\  A. k  e.  p  ( (
x  u.  { <. dom  x ,  z >. } ) `  suc  k )  e.  ( F `  ( ( x  u.  { <. dom  x ,  z >. } ) `  k
) ) ) )
223219, 222sylibr 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  /\  z  e.  ( F `  (
x `  m )
)  /\  ( z  e.  A  /\  (
x `  (/) )  =  C ) )  -> 
( x  u.  { <. dom  x ,  z
>. } )  e.  S
)
2242233coml 1212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( z  e.  A  /\  ( x `  (/) )  =  C )  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om ) )  -> 
( x  u.  { <. dom  x ,  z
>. } )  e.  S
)
2252243exp 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  e.  ( F `  ( x `  m
) )  ->  (
( z  e.  A  /\  ( x `  (/) )  =  C )  ->  (
( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
x  u.  { <. dom  x ,  z >. } )  e.  S
) ) )
226225expd 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  ( F `  ( x `  m
) )  ->  (
z  e.  A  -> 
( ( x `  (/) )  =  C  -> 
( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om )  ->  (
x  u.  { <. dom  x ,  z >. } )  e.  S
) ) ) )
22755, 226sylcom 30 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x `  (/) )  =  C  ->  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
x  u.  { <. dom  x ,  z >. } )  e.  S
) ) ) )
2282273impd 1219 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( ( z  e.  ( F `  ( x `  m
) )  /\  (
x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
)  ->  ( x  u.  { <. dom  x , 
z >. } )  e.  S ) )
229228ex 435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( x : suc  m --> A  -> 
( ( z  e.  ( F `  (
x `  m )
)  /\  ( x `  (/) )  =  C  /\  ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om ) )  -> 
( x  u.  { <. dom  x ,  z
>. } )  e.  S
) ) )
230229com23 81 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( (
z  e.  ( F `
 ( x `  m ) )  /\  ( x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
)  ->  ( x : suc  m --> A  -> 
( x  u.  { <. dom  x ,  z
>. } )  e.  S
) ) )
23151, 230mpdi 43 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( (
z  e.  ( F `
 ( x `  m ) )  /\  ( x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
)  ->  ( x  u.  { <. dom  x , 
z >. } )  e.  S ) )
232231imp 430 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( z  e.  ( F `  ( x `  m
) )  /\  (
x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
) )  ->  (
x  u.  { <. dom  x ,  z >. } )  e.  S
)
233 resundir 5081 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x ) )
234 frel 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x : suc  m --> A  ->  Rel  x )
235 resdm 5108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Rel  x  ->  ( x  |` 
dom  x )  =  x )
236234, 235syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x : suc  m --> A  -> 
( x  |`  dom  x
)  =  x )
237236adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( x  |`  dom  x )  =  x )
23870, 74sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  dom  x  e.  om )
23975, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( dom  x  e.  om  ->  -. 
dom  x  e.  dom  x )
240 incom 3598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { dom  x }  i^i  dom  x )  =  ( dom  x  i^i  { dom  x } )
241240eqeq1i 2433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( dom  x  i^i 
{ dom  x }
)  =  (/) )
24260, 61fnsn 5597 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  Fn  { dom  x }
243 fnresdisj 5647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( {
<. dom  x ,  z
>. }  Fn  { dom  x }  ->  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) ) )
244242, 243ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
245241, 244, 1073bitr3ri 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -. 
dom  x  e.  dom  x 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
246239, 245sylib 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  x  e.  om  ->  ( { <. dom  x , 
z >. }  |`  dom  x
)  =  (/) )
247238, 246syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. }  |`  dom  x )  =  (/) )
248237, 247uneq12d 3564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  ( x  u.  (/) ) )
249 un0 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  u.  (/) )  =  x
250248, 249syl6eq 2478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  x )
251233, 250syl5eq 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
252251ancoms 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
2532523adant1 1023 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
( x  u.  { <. dom  x ,  z
>. } )  |`  dom  x
)  =  x )
2542533ad2ant3 1028 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
)  ->  ( (
x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  x )
255254adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( z  e.  ( F `  ( x `  m
) )  /\  (
x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
) )  ->  (
( x  u.  { <. dom  x ,  z
>. } )  |`  dom  x
)  =  x )
256105uneq2i 3560 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  x  u.  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  u.  { dom  x } )
257 dmun 5003 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  ( dom  x  u.  dom  {
<. dom  x ,  z
>. } )
258 df-suc 5391 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  dom  x  =  ( dom  x  u.  { dom  x } )
259256, 257, 2583eqtr4i 2460 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
260255, 259jctil 539 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( z  e.  ( F `  ( x `  m
) )  /\  (
x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
) )  ->  ( dom  ( x  u.  { <. dom  x ,  z
>. } )  =  suc  dom  x  /\  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  x ) )
261 dmeq 4997 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  ->  dom  y  =  dom  ( x  u.  { <. dom  x ,  z >. } ) )
262261eqeq1d 2430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( dom  y  =  suc  dom  x  <->  dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
) )
263 reseq1 5061 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( y  |`  dom  x
)  =  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
) )
264263eqeq1d 2430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( y  |`  dom  x )  =  x  <-> 
( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )
265262, 264anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x )  <-> 
( dom  ( x  u.  { <. dom  x , 
z >. } )  =  suc  dom  x  /\  ( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) ) )
266265rspcev 3125 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( x  u.  { <. dom  x ,  z
>. } )  e.  S  /\  ( dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x  /\  ( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
267232, 260, 266syl2anc 665 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( z  e.  ( F `  ( x `  m
) )  /\  (
x `  (/) )  =  C  /\  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )
) )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
2682673exp2 1223 . . . . . . . . . . . . . . . . . . . 20  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  ( (
x `  (/) )  =  C  ->  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) ) ) )
269268exlimdv 1772 . . . . . . . . . . . . . . . . . . 19  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( E. z  z  e.  ( F `  ( x `  m ) )  -> 
( ( x `  (/) )  =  C  -> 
( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) ) ) )
270269adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( E. z 
z  e.  ( F `
 ( x `  m ) )  -> 
( ( x `  (/) )  =  C  -> 
( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  (
x `  k )
)  /\  x : suc  m --> A  /\  m  e.  om )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) ) ) )
27150, 270mpd 15 . . . . . . . . . . . . . . . . 17  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( ( x `
 (/) )  =  C  ->  ( ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  /\  x : suc  m --> A  /\  m  e.  om )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) )
272271com3r 82 . . . . . . . . . . . . . . . 16  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  (
( F : A --> ( ~P A  \  { (/)
} )  /\  x : suc  m --> A )  ->  ( ( x `
 (/) )  =  C  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) )
27336, 272mpan2d 678 . . . . . . . . . . . . . . 15  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  ( (
x `  (/) )  =  C  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) ) )
274273com3r 82 . . . . . . . . . . . . . 14  |-  ( ( x `  (/) )  =  C  ->  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) ) )
2752743expd 1222 . . . . . . . . . . . . 13  |-  ( ( x `  (/) )  =  C  ->  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
x : suc  m --> A  ->  ( m  e. 
om  ->  ( F : A
--> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) ) ) )
276275com3r 82 . . . . . . . . . . . 12  |-  ( x : suc  m --> A  -> 
( ( x `  (/) )  =  C  -> 
( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  ->  ( m  e. 
om  ->  ( F : A
--> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) ) ) )
2772763imp 1199 . . . . . . . . . . 11  |-  ( ( x : suc  m --> A  /\  ( x `  (/) )  =  C  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( m  e. 
om  ->  ( F : A
--> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) )
278277com12 32 . . . . . . . . . 10  |-  ( m  e.  om  ->  (
( x : suc  m
--> A  /\  ( x `
 (/) )  =  C  /\  A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) ) )
279278rexlimiv 2850 . . . . . . . . 9  |-  ( E. m  e.  om  (
x : suc  m --> A  /\  ( x `  (/) )  =  C  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( F : A
--> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) ) )
28035, 279sylbi 198 . . . . . . . 8  |-  ( x  e.  S  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) )
281280impcom 431 . . . . . . 7  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
282 rabn0 3725 . . . . . . 7  |-  ( { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  =/=  (/)  <->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) )
283281, 282sylibr 215 . . . . . 6  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =/=  (/) )
28430rabex 4518 . . . . . . . 8  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  _V
285284elsnc 3965 . . . . . . 7  |-  ( { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) }  <->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =  (/) )
286285necon3bbii 2648 . . . . . 6  |-  ( -. 
{ y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) }  e.  { (/) }  <->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) }  =/=  (/) )
287283, 286sylibr 215 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  -.  { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) } )
28833, 287eldifd 3390 . . . 4  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ( ~P S  \  { (/)
} ) )
289 axdc3lem4.3 . . . 4  |-  G  =  ( x  e.  S  |->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) } )
290288, 289fmptd 6005 . . 3  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  G : S
--> ( ~P S  \  { (/) } ) )
29130axdc2 8830 . . 3  |-  ( ( S  =/=  (/)  /\  G : S --> ( ~P S  \  { (/) } ) )  ->  E. h ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) ) )
29228, 290, 291syl2an 479 . 2  |-  ( ( C  e.  A  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. h
( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
29322, 23, 289axdc3lem2 8832 . 2  |-  ( 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 ) ) ) )
294292, 293syl 17 1  |-  ( ( C  e.  A  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  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:   -. wn 3    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1657    e. wcel 1872   {cab 2414    =/= wne 2599   A.wral 2714   E.wrex 2715   {crab 2718   _Vcvv 3022    \ cdif 3376    u. cun 3377    i^i cin 3378    C_ wss 3379   (/)c0 3704   ~Pcpw 3924   {csn 3941   <.cop 3947    |-> cmpt 4425   dom cdm 4796    |` cres 4798   Rel wrel 4801   Ord word 5384   suc csuc 5387   Fun wfun 5538    Fn wfn 5539   -->wf 5540   ` cfv 5544   omcom 6650
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-dc 8827
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-om 6651  df-1o 7137
This theorem is referenced by:  axdc3  8835
  Copyright terms: Public domain W3C validator