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

Theorem axdc3lem4 8824
Description: Lemma for axdc3 8825. 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 8817 (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 8817 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 8820. See axdc3lem2 8822 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 6692 . . . . . 6  |-  (/)  e.  om
2 eqid 2454 . . . . . . . . . 10  |-  { <. (/)
,  C >. }  =  { <. (/) ,  C >. }
3 fsng 6046 . . . . . . . . . . 11  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
41, 3mpan 668 . . . . . . . . . 10  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
52, 4mpbiri 233 . . . . . . . . 9  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> { C } )
6 snssi 4160 . . . . . . . . 9  |-  ( C  e.  A  ->  { C }  C_  A )
75, 6fssd 5722 . . . . . . . 8  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> A )
8 suc0 4941 . . . . . . . . 9  |-  suc  (/)  =  { (/)
}
98feq2i 5706 . . . . . . . 8  |-  ( {
<. (/) ,  C >. } : suc  (/) --> A  <->  { <. (/) ,  C >. } : { (/) } --> A )
107, 9sylibr 212 . . . . . . 7  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : suc  (/) --> A )
11 fvsng 6081 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
121, 11mpan 668 . . . . . . 7  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
13 ral0 3922 . . . . . . . 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 1174 . . . . . 6  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )
16 suceq 4932 . . . . . . . . 9  |-  ( m  =  (/)  ->  suc  m  =  suc  (/) )
1716feq2d 5700 . . . . . . . 8  |-  ( m  =  (/)  ->  ( {
<. (/) ,  C >. } : suc  m --> A  <->  { <. (/) ,  C >. } : suc  (/) --> A ) )
18 raleq 3051 . . . . . . . 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 1299 . . . . . . 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 3207 . . . . . 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 661 . . . . 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 4678 . . . . . 6  |-  { <. (/)
,  C >. }  e.  _V
2522, 23, 24axdc3lem3 8823 . . . . 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 212 . . . 4  |-  ( C  e.  A  ->  { <. (/)
,  C >. }  e.  S )
27 ne0i 3789 . . . 4  |-  ( {
<. (/) ,  C >. }  e.  S  ->  S  =/=  (/) )
2826, 27syl 16 . . 3  |-  ( C  e.  A  ->  S  =/=  (/) )
29 ssrab2 3571 . . . . . . 7  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S
3022, 23axdc3lem 8821 . . . . . . . 8  |-  S  e. 
_V
3130elpw2 4601 . . . . . . 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 209 . . . . . 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 3109 . . . . . . . . . 10  |-  x  e. 
_V
3522, 23, 34axdc3lem3 8823 . . . . . . . . 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 995 . . . . . . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . . . . . . 22  |-  m  e. 
_V
3837sucid 4946 . . . . . . . . . . . . . . . . . . . . 21  |-  m  e. 
suc  m
39 ffvelrn 6005 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x : suc  m --> A  /\  m  e.  suc  m )  ->  (
x `  m )  e.  A )
4038, 39mpan2 669 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : suc  m --> A  -> 
( x `  m
)  e.  A )
41 ffvelrn 6005 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( x `
 m )  e.  A )  ->  ( F `  ( x `  m ) )  e.  ( ~P A  \  { (/) } ) )
4240, 41sylan2 472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( F `  ( x `  m
) )  e.  ( ~P A  \  { (/)
} ) )
43 eldifn 3613 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  -.  ( F `  (
x `  m )
)  e.  { (/) } )
44 fvex 5858 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( x `  m ) )  e. 
_V
4544elsnc 4040 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( x `
 m ) )  e.  { (/) }  <->  ( F `  ( x `  m
) )  =  (/) )
4645necon3bbii 2715 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <-> 
( F `  (
x `  m )
)  =/=  (/) )
47 n0 3793 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  ( x `
 m ) )  =/=  (/)  <->  E. z  z  e.  ( F `  (
x `  m )
) )
4846, 47bitri 249 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <->  E. z  z  e.  ( F `  ( x `
 m ) ) )
4943, 48sylib 196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5042, 49syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  E. z  z  e.  ( F `  (
x `  m )
) )
51 simp32 1031 . . . . . . . . . . . . . . . . . . . . . . . 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 3612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  -> 
( F `  (
x `  m )
)  e.  ~P A
)
53 elelpwi 4010 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( F `  ( x `
 m ) )  e.  ~P A )  ->  z  e.  A
)
5453expcom 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ~P A  -> 
( z  e.  ( F `  ( x `
 m ) )  ->  z  e.  A
) )
5542, 52, 543syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  z  e.  A ) )
56 peano2 6693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  om  ->  suc  m  e.  om )
57563ad2ant3 1017 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  suc  m  e.  om )
58573ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  x : suc  m --> A )
6034dmex 6706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  dom  x  e.  _V
61 vex 3109 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  z  e. 
_V
62 eqid 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  { <. dom  x ,  z >. }  =  { <. dom  x ,  z >. }
63 fsng 6046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  ( { <. dom  x ,  z >. } : { dom  x } --> { z }  <->  { <. dom  x , 
z >. }  =  { <. dom  x ,  z
>. } ) )
6462, 63mpbiri 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  { <. dom  x , 
z >. } : { dom  x } --> { z } )
6560, 61, 64mp2an 670 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  { <. dom  x ,  z >. } : { dom  x }
--> { z }
66 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  z  e.  A )
6766snssd 4161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { z }  C_  A )
68 fss 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( { <. dom  x , 
z >. } : { dom  x } --> { z }  /\  { z }  C_  A )  ->  { <. dom  x , 
z >. } : { dom  x } --> A )
6965, 67, 68sylancr 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { <. dom  x ,  z >. } : { dom  x }
--> A )
70 fdm 5717 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  dom  x  =  suc  m
)
7156adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  suc  m  e. 
om )
72 eleq1 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
om 
<->  suc  m  e.  om ) )
7372adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  om  <->  suc  m  e. 
om ) )
7471, 73mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  dom  x  e. 
om )
75 nnord 6681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  e.  om  ->  Ord 
dom  x )
76 ordirr 4885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( Ord 
dom  x  ->  -.  dom  x  e.  dom  x
)
7774, 75, 763syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  dom  x )
78 eleq2 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
dom  x  <->  dom  x  e. 
suc  m ) )
7978adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  dom  x  <->  dom  x  e. 
suc  m ) )
8077, 79mtbid 298 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  suc  m )
81 disjsn 4076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( suc  m  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
suc  m )
8280, 81sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
8370, 82sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( suc  m  i^i  { dom  x }
)  =  (/) )
8483adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
85 fun2 5731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : ( suc  m  u.  { dom  x } ) --> A )
87 sneq 4026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( dom  x  =  suc  m  ->  { dom  x }  =  { suc  m }
)
8887uneq2d 3644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  ( suc  m  u.  { suc  m } ) )
89 df-suc 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  suc  suc  m  =  ( suc  m  u.  { suc  m } )
9088, 89syl6eqr 2513 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  suc  suc  m )
9170, 90syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( suc  m  u.  { dom  x } )  =  suc  suc  m
)
9291ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  u.  { dom  x } )  =  suc  suc  m )
9392feq2d 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A )
9594ex 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  A  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
9695adantrd 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( z  e.  A  /\  (
x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) )
9796a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  Fun  x )
102101adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  x )
10360, 61funsn 5618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  Fun  { <. dom  x ,  z
>. }
104102, 103jctir 536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( Fun  x  /\  Fun  { <. dom  x ,  z >. } ) )
10561dmsnop 5465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  dom  { <. dom  x ,  z
>. }  =  { dom  x }
106105ineq2i 3683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  i^i  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  i^i  { dom  x } )
107 disjsn 4076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
dom  x )
10877, 107sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  { dom  x } )  =  (/) )
109106, 108syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
11070, 109sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
111 funun 5612 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( Fun  x  /\  Fun  { <. dom  x , 
z >. } )  /\  ( dom  x  i^i  dom  {
<. dom  x ,  z
>. } )  =  (/) )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
112104, 110, 111syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
113 ssun1 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  om  ->  Ord  m )
116 0elsuc 6643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( Ord  m  ->  (/)  e.  suc  m )
117115, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  om  ->  (/)  e.  suc  m )
118117adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  suc  m
)
11970eleq2d 2524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( (/)  e.  dom  x  <->  (/)  e.  suc  m ) )
120119adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( (/)  e.  dom  x 
<->  (/)  e.  suc  m ) )
121118, 120mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  dom  x
)
122 funssfv 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 (/) )  =  ( x `  (/) ) )
124123eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
125124ancoms 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
1261253adant1 1012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )
131 nfv 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  x : suc  m --> A
132 nfv 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  m  e.  om
133130, 131, 132nf3an 1935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )
134 nfv 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k  z  e.  ( F `
 ( x `  m ) )
135 nfv 1712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( z  e.  A  /\  ( x `  (/) )  =  C )
136133, 134, 135nf3an 1935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 753 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  suc  m  -> 
( k  e.  m  \/  k  =  m
) )
139 rsp 2820 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
k  e.  m  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) ) )
140139impcom 428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( k  e.  m  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
141140ad2ant2lr 745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( Ord  m  ->  ( k  e.  m  <->  suc  k  e.  suc  m ) )
146115, 145syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( m  e.  om  ->  (
k  e.  m  <->  suc  k  e. 
suc  m ) )
147146biimpa 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  m )  ->  suc  k  e.  suc  m )
148 eleq2 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  m  ->  ( suc  k  e. 
dom  x  <->  suc  k  e. 
suc  m ) )
149148biimparc 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( suc  k  e.  suc  m  /\  dom  x  =  suc  m )  ->  suc  k  e.  dom  x )
150147, 70, 149syl2an 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  suc  k  e.  dom  x )
151 funssfv 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1531523adant2 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( dom  x  =  suc  m  ->  ( k  e.  dom  x 
<->  k  e.  suc  m
) )
157156biimparc 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  e.  suc  m  /\  dom  x  =  suc  m )  ->  k  e.  dom  x )
15870, 157sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
1591583adant1 1012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
160 funssfv 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
1621613adant1r 1219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
163162fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
171 ssun2 3654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( k  =  m  ->  suc  k  =  suc  m )
174173eqeq2d 2468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( k  =  m  ->  ( dom  x  =  suc  k  <->  dom  x  =  suc  m
) )
175174biimpar 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  dom  x  =  suc  k )
17660snid 4044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  dom  x  e.  { dom  x }
177176, 105eleqtrri 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  dom  x  e.  dom  { <. dom  x ,  z >. }
178175, 177syl6eqelr 2551 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  suc  k  e. 
dom  { <. dom  x , 
z >. } )
17970, 178sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
1801793adant2 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
181 funssfv 5863 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  ( { <. dom  x ,  z >. } `  suc  k ) )
1831753adant2 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  dom  x  =  suc  k )
18460, 61fvsn 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( {
<. dom  x ,  z
>. } `  dom  x
)  =  z
185 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  dom  x )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
186184, 185syl5reqr 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
187183, 186syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
18870, 187syl3an3 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
189182, 188eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  z )
1901893expa 1194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1911903adant2 1013 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1921613adant1l 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
193 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( k  =  m  ->  (
x `  k )  =  ( x `  m ) )
194193adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( x `  k
)  =  ( x `
 m ) )
1951943ad2ant1 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
x `  k )  =  ( x `  m ) )
196192, 195eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 m ) )
197196fveq2d 5852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2536 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 79 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 433 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 31 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4932 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( p  =  suc  m  ->  suc  p  =  suc  suc  m )
215214feq2d 5700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  <->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
216 raleq 3051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1299 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  e.  _V
22134, 220unex 6571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  u.  { <. dom  x ,  z >. } )  e.  _V
22222, 23, 221axdc3lem3 8823 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 29 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1208 . . . . . . . . . . . . . . . . . . . . . . . . . 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 432 . . . . . . . . . . . . . . . . . . . . . . . . 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 78 . . . . . . . . . . . . . . . . . . . . . . . 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 42 . . . . . . . . . . . . . . . . . . . . . . 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 427 . . . . . . . . . . . . . . . . . . . . . 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 5276 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x ) )
234 frel 5716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x : suc  m --> A  ->  Rel  x )
235 resdm 5303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Rel  x  ->  ( x  |` 
dom  x )  =  x )
236234, 235syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x : suc  m --> A  -> 
( x  |`  dom  x
)  =  x )
237236adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( x  |`  dom  x )  =  x )
23870, 74sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  dom  x  e.  om )
23975, 76syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( dom  x  e.  om  ->  -. 
dom  x  e.  dom  x )
240 incom 3677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { dom  x }  i^i  dom  x )  =  ( dom  x  i^i  { dom  x } )
241240eqeq1i 2461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( dom  x  i^i 
{ dom  x }
)  =  (/) )
24260, 61fnsn 5623 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  Fn  { dom  x }
243 fnresdisj 5673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -. 
dom  x  e.  dom  x 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
246239, 245sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  x  e.  om  ->  ( { <. dom  x , 
z >. }  |`  dom  x
)  =  (/) )
247238, 246syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. }  |`  dom  x )  =  (/) )
248237, 247uneq12d 3645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  ( x  u.  (/) ) )
249 un0 3809 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  u.  (/) )  =  x
250248, 249syl6eq 2511 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  x )
251233, 250syl5eq 2507 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
252251ancoms 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
2532523adant1 1012 . . . . . . . . . . . . . . . . . . . . . . . . 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 1017 . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . 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 3641 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  x  u.  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  u.  { dom  x } )
257 dmun 5198 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  ( dom  x  u.  dom  {
<. dom  x ,  z
>. } )
258 df-suc 4873 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  dom  x  =  ( dom  x  u.  { dom  x } )
259256, 257, 2583eqtr4i 2493 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
260255, 259jctil 535 . . . . . . . . . . . . . . . . . . . . . 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 5192 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  ->  dom  y  =  dom  ( x  u.  { <. dom  x ,  z >. } ) )
262261eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( dom  y  =  suc  dom  x  <->  dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
) )
263 reseq1 5256 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( y  |`  dom  x
)  =  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
) )
264263eqeq1d 2456 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( y  |`  dom  x )  =  x  <-> 
( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )
265262, 264anbi12d 708 . . . . . . . . . . . . . . . . . . . . . . 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 3207 . . . . . . . . . . . . . . . . . . . . . 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 659 . . . . . . . . . . . . . . . . . . . . 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 1212 . . . . . . . . . . . . . . . . . . . 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 1729 . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . 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 79 . . . . . . . . . . . . . . . 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 672 . . . . . . . . . . . . . . 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 79 . . . . . . . . . . . . . 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 1211 . . . . . . . . . . . . 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 79 . . . . . . . . . . . 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 1188 . . . . . . . . . . 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 31 . . . . . . . . . 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 2940 . . . . . . . . 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 195 . . . . . . . 8  |-  ( x  e.  S  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) )
281280impcom 428 . . . . . . 7  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
282 rabn0 3804 . . . . . . 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 212 . . . . . 6  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =/=  (/) )
28430rabex 4588 . . . . . . . 8  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  _V
285284elsnc 4040 . . . . . . 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 2715 . . . . . 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 212 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  -.  { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) } )
28833, 287eldifd 3472 . . . 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 6031 . . 3  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  G : S
--> ( ~P S  \  { (/) } ) )
29130axdc2 8820 . . 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 475 . 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 8822 . 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 16 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 184    \/ wo 366    /\ wa 367    /\ w3a 971    = wceq 1398   E.wex 1617    e. wcel 1823   {cab 2439    =/= wne 2649   A.wral 2804   E.wrex 2805   {crab 2808   _Vcvv 3106    \ cdif 3458    u. cun 3459    i^i cin 3460    C_ wss 3461   (/)c0 3783   ~Pcpw 3999   {csn 4016   <.cop 4022    |-> cmpt 4497   Ord word 4866   suc csuc 4869   dom cdm 4988    |` cres 4990   Rel wrel 4993   Fun wfun 5564    Fn wfn 5565   -->wf 5566   ` cfv 5570   omcom 6673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-dc 8817
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-reu 2811  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-uni 4236  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-om 6674  df-1o 7122
This theorem is referenced by:  axdc3  8825
  Copyright terms: Public domain W3C validator