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

Theorem axdc3lem4 8334
Description: Lemma for axdc3 8335. 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 8327 (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 8327 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 8330. See axdc3lem2 8332 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 4865 . . . . . 6  |-  (/)  e.  om
2 eqid 2437 . . . . . . . . . 10  |-  { <. (/)
,  C >. }  =  { <. (/) ,  C >. }
3 fsng 5908 . . . . . . . . . . 11  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
41, 3mpan 653 . . . . . . . . . 10  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
52, 4mpbiri 226 . . . . . . . . 9  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> { C } )
6 snssi 3943 . . . . . . . . 9  |-  ( C  e.  A  ->  { C }  C_  A )
7 fss 5600 . . . . . . . . 9  |-  ( ( { <. (/) ,  C >. } : { (/) } --> { C }  /\  { C }  C_  A )  ->  { <. (/)
,  C >. } : { (/) } --> A )
85, 6, 7syl2anc 644 . . . . . . . 8  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> A )
9 suc0 4656 . . . . . . . . 9  |-  suc  (/)  =  { (/)
}
109feq2i 5587 . . . . . . . 8  |-  ( {
<. (/) ,  C >. } : suc  (/) --> A  <->  { <. (/) ,  C >. } : { (/) } --> A )
118, 10sylibr 205 . . . . . . 7  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : suc  (/) --> A )
12 fvsng 5928 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
131, 12mpan 653 . . . . . . 7  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
14 ral0 3733 . . . . . . . 8  |-  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) )
1514a1i 11 . . . . . . 7  |-  ( C  e.  A  ->  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) )
1611, 13, 153jca 1135 . . . . . 6  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )
17 suceq 4647 . . . . . . . . 9  |-  ( m  =  (/)  ->  suc  m  =  suc  (/) )
1817feq2d 5582 . . . . . . . 8  |-  ( m  =  (/)  ->  ( {
<. (/) ,  C >. } : suc  m --> A  <->  { <. (/) ,  C >. } : suc  (/) --> A ) )
19 raleq 2905 . . . . . . . 8  |-  ( m  =  (/)  ->  ( A. k  e.  m  ( { <. (/) ,  C >. } `
 suc  k )  e.  ( F `  ( { <. (/) ,  C >. } `
 k ) )  <->  A. k  e.  (/)  ( {
<. (/) ,  C >. } `
 suc  k )  e.  ( F `  ( { <. (/) ,  C >. } `
 k ) ) ) )
2018, 193anbi13d 1257 . . . . . . 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 ) ) ) ) )
2120rspcev 3053 . . . . . 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 ) ) ) )
221, 16, 21sylancr 646 . . . . 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 ) ) ) )
23 axdc3lem4.1 . . . . . 6  |-  A  e. 
_V
24 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 ) ) ) }
25 snex 4406 . . . . . 6  |-  { <. (/)
,  C >. }  e.  _V
2623, 24, 25axdc3lem3 8333 . . . . 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 ) ) ) )
2722, 26sylibr 205 . . . 4  |-  ( C  e.  A  ->  { <. (/)
,  C >. }  e.  S )
28 ne0i 3635 . . . 4  |-  ( {
<. (/) ,  C >. }  e.  S  ->  S  =/=  (/) )
2927, 28syl 16 . . 3  |-  ( C  e.  A  ->  S  =/=  (/) )
30 ssrab2 3429 . . . . . . 7  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S
3123, 24axdc3lem 8331 . . . . . . . 8  |-  S  e. 
_V
3231elpw2 4365 . . . . . . 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 )
3330, 32mpbir 202 . . . . . 6  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ~P S
3433a1i 11 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ~P S )
35 vex 2960 . . . . . . . . . 10  |-  x  e. 
_V
3623, 24, 35axdc3lem3 8333 . . . . . . . . 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 )
) ) )
37 simp2 959 . . . . . . . . . . . . . . . 16  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  x : suc  m --> A )
38 vex 2960 . . . . . . . . . . . . . . . . . . . . . 22  |-  m  e. 
_V
3938sucid 4661 . . . . . . . . . . . . . . . . . . . . 21  |-  m  e. 
suc  m
40 ffvelrn 5869 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x : suc  m --> A  /\  m  e.  suc  m )  ->  (
x `  m )  e.  A )
4139, 40mpan2 654 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : suc  m --> A  -> 
( x `  m
)  e.  A )
42 ffvelrn 5869 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( x `
 m )  e.  A )  ->  ( F `  ( x `  m ) )  e.  ( ~P A  \  { (/) } ) )
4341, 42sylan2 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( F `  ( x `  m
) )  e.  ( ~P A  \  { (/)
} ) )
44 eldifn 3471 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  -.  ( F `  (
x `  m )
)  e.  { (/) } )
45 fvex 5743 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( x `  m ) )  e. 
_V
4645elsnc 3838 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( x `
 m ) )  e.  { (/) }  <->  ( F `  ( x `  m
) )  =  (/) )
4746necon3bbii 2633 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <-> 
( F `  (
x `  m )
)  =/=  (/) )
48 n0 3638 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  ( x `
 m ) )  =/=  (/)  <->  E. z  z  e.  ( F `  (
x `  m )
) )
4947, 48bitri 242 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5044, 49sylib 190 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5143, 50syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  E. z  z  e.  ( F `  (
x `  m )
) )
52 simp32 995 . . . . . . . . . . . . . . . . . . . . . . . 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 )
53 eldifi 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  -> 
( F `  (
x `  m )
)  e.  ~P A
)
54 elelpwi 3810 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( F `  ( x `
 m ) )  e.  ~P A )  ->  z  e.  A
)
5554expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ~P A  -> 
( z  e.  ( F `  ( x `
 m ) )  ->  z  e.  A
) )
5643, 53, 553syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  z  e.  A ) )
57 peano2 4866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  om  ->  suc  m  e.  om )
58573ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  suc  m  e.  om )
59583ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
60 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  x : suc  m --> A )
6135dmex 5133 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  dom  x  e.  _V
62 vex 2960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  z  e. 
_V
63 eqid 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  { <. dom  x ,  z >. }  =  { <. dom  x ,  z >. }
64 fsng 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  ( { <. dom  x ,  z >. } : { dom  x } --> { z }  <->  { <. dom  x , 
z >. }  =  { <. dom  x ,  z
>. } ) )
6563, 64mpbiri 226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  { <. dom  x , 
z >. } : { dom  x } --> { z } )
6661, 62, 65mp2an 655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  { <. dom  x ,  z >. } : { dom  x }
--> { z }
67 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  z  e.  A )
6867snssd 3944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { z }  C_  A )
69 fss 5600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( { <. dom  x , 
z >. } : { dom  x } --> { z }  /\  { z }  C_  A )  ->  { <. dom  x , 
z >. } : { dom  x } --> A )
7066, 68, 69sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { <. dom  x ,  z >. } : { dom  x }
--> A )
71 fdm 5596 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  dom  x  =  suc  m
)
7257adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  suc  m  e. 
om )
73 eleq1 2497 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
om 
<->  suc  m  e.  om ) )
7473adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  om  <->  suc  m  e. 
om ) )
7572, 74mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  dom  x  e. 
om )
76 nnord 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  e.  om  ->  Ord 
dom  x )
77 ordirr 4600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( Ord 
dom  x  ->  -.  dom  x  e.  dom  x
)
7875, 76, 773syl 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  dom  x )
79 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
dom  x  <->  dom  x  e. 
suc  m ) )
8079adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  dom  x  <->  dom  x  e. 
suc  m ) )
8178, 80mtbid 293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  suc  m )
82 disjsn 3869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( suc  m  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
suc  m )
8381, 82sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
8471, 83sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( suc  m  i^i  { dom  x }
)  =  (/) )
8584adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
86 fun2 5609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
8760, 70, 85, 86syl21anc 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : ( suc  m  u.  { dom  x } ) --> A )
88 sneq 3826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( dom  x  =  suc  m  ->  { dom  x }  =  { suc  m }
)
8988uneq2d 3502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  ( suc  m  u.  { suc  m } ) )
90 df-suc 4588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  suc  suc  m  =  ( suc  m  u.  { suc  m } )
9189, 90syl6eqr 2487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  suc  suc  m )
9271, 91syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( suc  m  u.  { dom  x } )  =  suc  suc  m
)
9392ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  u.  { dom  x } )  =  suc  suc  m )
9493feq2d 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
9587, 94mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A )
9695ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  A  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
9796adantrd 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( z  e.  A  /\  (
x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) )
9897a1d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
9998ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
100993adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
1011003imp 1148 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
102 ffun 5594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  Fun  x )
103102adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  x )
10461, 62funsn 5500 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  Fun  { <. dom  x ,  z
>. }
105103, 104jctir 526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( Fun  x  /\  Fun  { <. dom  x ,  z >. } ) )
10662dmsnop 5345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  dom  { <. dom  x ,  z
>. }  =  { dom  x }
107106ineq2i 3540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  i^i  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  i^i  { dom  x } )
108 disjsn 3869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
dom  x )
10978, 108sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  { dom  x } )  =  (/) )
110107, 109syl5eq 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
11171, 110sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
112 funun 5496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( Fun  x  /\  Fun  { <. dom  x , 
z >. } )  /\  ( dom  x  i^i  dom  {
<. dom  x ,  z
>. } )  =  (/) )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
113105, 111, 112syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
114 ssun1 3511 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  x  C_  ( x  u.  { <. dom  x ,  z >. } )
115114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
116 nnord 4854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  om  ->  Ord  m )
117 0elsuc 4816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( Ord  m  ->  (/)  e.  suc  m )
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  om  ->  (/)  e.  suc  m )
119118adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  suc  m
)
12071eleq2d 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( (/)  e.  dom  x  <->  (/)  e.  suc  m ) )
121120adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( (/)  e.  dom  x 
<->  (/)  e.  suc  m ) )
122119, 121mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  dom  x
)
123 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( Fun  ( x  u. 
{ <. dom  x , 
z >. } )  /\  x  C_  ( x  u. 
{ <. dom  x , 
z >. } )  /\  (/) 
e.  dom  x )  ->  ( ( x  u. 
{ <. dom  x , 
z >. } ) `  (/) )  =  ( x `
 (/) ) )
124113, 115, 122, 123syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 (/) )  =  ( x `  (/) ) )
125124eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
126125ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
1271263adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
128127biimpar 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
129128adantrl 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
1301293adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
131 nfra1 2757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )
132 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  x : suc  m --> A
133 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  m  e.  om
134131, 132, 133nf3an 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )
135 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k  z  e.  ( F `
 ( x `  m ) )
136 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( z  e.  A  /\  ( x `  (/) )  =  C )
137134, 135, 136nf3an 1850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
138 simplr 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  k  e.  suc  m )  /\  x : suc  m --> A )  ->  k  e.  suc  m )
139 elsuci 4648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  suc  m  -> 
( k  e.  m  \/  k  =  m
) )
140 rsp 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
k  e.  m  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) ) )
141140impcom 421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( k  e.  m  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
142141ad2ant2lr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
1431423adant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
144113adantlr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  Fun  ( x  u.  { <. dom  x ,  z >. } ) )
145114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  x  C_  ( x  u.  { <. dom  x ,  z
>. } ) )
146 ordsucelsuc 4803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( Ord  m  ->  ( k  e.  m  <->  suc  k  e.  suc  m ) )
147116, 146syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( m  e.  om  ->  (
k  e.  m  <->  suc  k  e. 
suc  m ) )
148147biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  m )  ->  suc  k  e.  suc  m )
149 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  m  ->  ( suc  k  e. 
dom  x  <->  suc  k  e. 
suc  m ) )
150149biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( suc  k  e.  suc  m  /\  dom  x  =  suc  m )  ->  suc  k  e.  dom  x )
151148, 71, 150syl2an 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  suc  k  e.  dom  x )
152 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
153144, 145, 151, 152syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1541533adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
1551133adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
156114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
157 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( dom  x  =  suc  m  ->  ( k  e.  dom  x 
<->  k  e.  suc  m
) )
158157biimparc 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  e.  suc  m  /\  dom  x  =  suc  m )  ->  k  e.  dom  x )
15971, 158sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
1601593adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
161 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
162155, 156, 160, 161syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
1631623adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
164163fveq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
165154, 164eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
1661653adant2l 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
167143, 166mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
168167a1d 24 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
1691683expib 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
170169expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
1711133adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
172 ssun2 3512 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  { <. dom  x ,  z >. }  C_  ( x  u. 
{ <. dom  x , 
z >. } )
173172a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  { <. dom  x ,  z >. }  C_  ( x  u.  { <. dom  x ,  z >. } ) )
174 suceq 4647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( k  =  m  ->  suc  k  =  suc  m )
175174eqeq2d 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( k  =  m  ->  ( dom  x  =  suc  k  <->  dom  x  =  suc  m
) )
176175biimpar 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  dom  x  =  suc  k )
17761snid 3842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  dom  x  e.  { dom  x }
178177, 106eleqtrri 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  dom  x  e.  dom  { <. dom  x ,  z >. }
179176, 178syl6eqelr 2526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  suc  k  e. 
dom  { <. dom  x , 
z >. } )
18071, 179sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
1811803adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
182 funssfv 5747 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
183171, 173, 181, 182syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  ( { <. dom  x ,  z >. } `  suc  k ) )
1841763adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  dom  x  =  suc  k )
18561, 62fvsn 5927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( {
<. dom  x ,  z
>. } `  dom  x
)  =  z
186 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  dom  x )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
187185, 186syl5reqr 2484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
188184, 187syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
18971, 188syl3an3 1220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
190183, 189eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  z )
1911903expa 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1921913adant2 977 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1931623adant1l 1177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
194 fveq2 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( k  =  m  ->  (
x `  k )  =  ( x `  m ) )
195194adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( x `  k
)  =  ( x `
 m ) )
1961953ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
x `  k )  =  ( x `  m ) )
197193, 196eqtrd 2469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 m ) )
198197fveq2d 5733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  ( F `  ( (
x  u.  { <. dom  x ,  z >. } ) `  k
) )  =  ( F `  ( x `
 m ) ) )
199192, 198eleq12d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
2001993adant2l 1179 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
201200biimprd 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
2022013expib 1157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
203202ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
204170, 203jaoi 370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
205139, 204syl 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
) ) ) ) ) )
206205com3r 76 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
207138, 206mpd 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
) ) ) ) )
208207ex 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) )
209208expcom 426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) ) ) )
2102093impd 1168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
211210imp3a 422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
212211com12 30 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
2132123adant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
214137, 213ralrimi 2788 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
215 suceq 4647 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( p  =  suc  m  ->  suc  p  =  suc  suc  m )
216215feq2d 5582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  <->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
217 raleq 2905 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
218216, 2173anbi13d 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) ) )
219218rspcev 3053 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
22059, 101, 130, 214, 219syl13anc 1187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
221 snex 4406 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  e.  _V
22235, 221unex 4708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  u.  { <. dom  x ,  z >. } )  e.  _V
22323, 24, 222axdc3lem3 8333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
224220, 223sylibr 205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
2252243coml 1161 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
)
2262253exp 1153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
227226exp3a 427 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
22856, 227sylcom 28 . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) ) )
2292283impd 1168 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
230229ex 425 . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
231230com23 75 . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
23252, 231mpdi 41 . . . . . . . . . . . . . . . . . . . . . . 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 ) )
233232imp 420 . . . . . . . . . . . . . . . . . . . . . 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
)
234 resundir 5162 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x ) )
235 frel 5595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x : suc  m --> A  ->  Rel  x )
236 resdm 5185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Rel  x  ->  ( x  |` 
dom  x )  =  x )
237235, 236syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x : suc  m --> A  -> 
( x  |`  dom  x
)  =  x )
238237adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( x  |`  dom  x )  =  x )
23971, 75sylan2 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  dom  x  e.  om )
24076, 77syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( dom  x  e.  om  ->  -. 
dom  x  e.  dom  x )
241 incom 3534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { dom  x }  i^i  dom  x )  =  ( dom  x  i^i  { dom  x } )
242241eqeq1i 2444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( dom  x  i^i 
{ dom  x }
)  =  (/) )
24361, 62fnsn 5505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  Fn  { dom  x }
244 fnresdisj 5556 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( {
<. dom  x ,  z
>. }  Fn  { dom  x }  ->  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) ) )
245243, 244ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
246242, 245, 1083bitr3ri 269 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -. 
dom  x  e.  dom  x 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
247240, 246sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  x  e.  om  ->  ( { <. dom  x , 
z >. }  |`  dom  x
)  =  (/) )
248239, 247syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. }  |`  dom  x )  =  (/) )
249238, 248uneq12d 3503 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  ( x  u.  (/) ) )
250 un0 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  u.  (/) )  =  x
251249, 250syl6eq 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  x )
252234, 251syl5eq 2481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
253252ancoms 441 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
2542533adant1 976 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
2552543ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . 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 )
256255adantl 454 . . . . . . . . . . . . . . . . . . . . . . 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 )
257106uneq2i 3499 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  x  u.  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  u.  { dom  x } )
258 dmun 5077 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  ( dom  x  u.  dom  {
<. dom  x ,  z
>. } )
259 df-suc 4588 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  dom  x  =  ( dom  x  u.  { dom  x } )
260257, 258, 2593eqtr4i 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
261256, 260jctil 525 . . . . . . . . . . . . . . . . . . . . . 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 ) )
262 dmeq 5071 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  ->  dom  y  =  dom  ( x  u.  { <. dom  x ,  z >. } ) )
263262eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( dom  y  =  suc  dom  x  <->  dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
) )
264 reseq1 5141 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( y  |`  dom  x
)  =  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
) )
265264eqeq1d 2445 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( y  |`  dom  x )  =  x  <-> 
( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )
266263, 265anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
267266rspcev 3053 . . . . . . . . . . . . . . . . . . . . . 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 ) )
268233, 261, 267syl2anc 644 . . . . . . . . . . . . . . . . . . . . 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 ) )
2692683exp2 1172 . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
270269exlimdv 1647 . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
271270adantr 453 . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
27251, 271mpd 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 ) ) ) )
273272com3r 76 . . . . . . . . . . . . . . . 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 ) ) ) )
27437, 273mpan2d 657 . . . . . . . . . . . . . . 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 ) ) ) )
275274com3r 76 . . . . . . . . . . . . . 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 ) ) ) )
2762753expd 1171 . . . . . . . . . . . . 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 ) ) ) ) ) )
277276com3r 76 . . . . . . . . . . . 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 ) ) ) ) ) )
2782773imp 1148 . . . . . . . . . . 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 ) ) ) )
279278com12 30 . . . . . . . . . 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 ) ) ) )
280279rexlimiv 2825 . . . . . . . . 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 ) ) )
28136, 280sylbi 189 . . . . . . . 8  |-  ( x  e.  S  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) )
282281impcom 421 . . . . . . 7  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
283 rabn0 3648 . . . . . . 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 ) )
284282, 283sylibr 205 . . . . . 6  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =/=  (/) )
28531rabex 4355 . . . . . . . 8  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  _V
286285elsnc 3838 . . . . . . 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 ) }  =  (/) )
287286necon3bbii 2633 . . . . . 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 ) }  =/=  (/) )
288284, 287sylibr 205 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  -.  { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) } )
28934, 288eldifd 3332 . . . 4  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ( ~P S  \  { (/)
} ) )
290 axdc3lem4.3 . . . 4  |-  G  =  ( x  e.  S  |->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) } )
291289, 290fmptd 5894 . . 3  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  G : S
--> ( ~P S  \  { (/) } ) )
29231axdc2 8330 . . 3  |-  ( ( S  =/=  (/)  /\  G : S --> ( ~P S  \  { (/) } ) )  ->  E. h ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) ) )
29329, 291, 292syl2an 465 . 2  |-  ( ( C  e.  A  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. h
( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
29423, 24, 290axdc3lem2 8332 . 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 ) ) ) )
295293, 294syl 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 set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    /\ w3a 937   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2423    =/= wne 2600   A.wral 2706   E.wrex 2707   {crab 2710   _Vcvv 2957    \ cdif 3318    u. cun 3319    i^i cin 3320    C_ wss 3321   (/)c0 3629   ~Pcpw 3800   {csn 3815   <.cop 3818    e. cmpt 4267   Ord word 4581   suc csuc 4584   omcom 4846   dom cdm 4879    |` cres 4881   Rel wrel 4884   Fun wfun 5449    Fn wfn 5450   -->wf 5451   ` cfv 5455
This theorem is referenced by:  axdc3  8335
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-dc 8327
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-1o 6725
  Copyright terms: Public domain W3C validator