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

Theorem axdc3lem4 8618
Description: Lemma for axdc3 8619. 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 8611 (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 8611 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 8614. See axdc3lem2 8616 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 6494 . . . . . 6  |-  (/)  e.  om
2 eqid 2441 . . . . . . . . . 10  |-  { <. (/)
,  C >. }  =  { <. (/) ,  C >. }
3 fsng 5879 . . . . . . . . . . 11  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
41, 3mpan 665 . . . . . . . . . 10  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
52, 4mpbiri 233 . . . . . . . . 9  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> { C } )
6 snssi 4014 . . . . . . . . 9  |-  ( C  e.  A  ->  { C }  C_  A )
7 fss 5564 . . . . . . . . 9  |-  ( ( { <. (/) ,  C >. } : { (/) } --> { C }  /\  { C }  C_  A )  ->  { <. (/)
,  C >. } : { (/) } --> A )
85, 6, 7syl2anc 656 . . . . . . . 8  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> A )
9 suc0 4789 . . . . . . . . 9  |-  suc  (/)  =  { (/)
}
109feq2i 5549 . . . . . . . 8  |-  ( {
<. (/) ,  C >. } : suc  (/) --> A  <->  { <. (/) ,  C >. } : { (/) } --> A )
118, 10sylibr 212 . . . . . . 7  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : suc  (/) --> A )
12 fvsng 5909 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
131, 12mpan 665 . . . . . . 7  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
14 ral0 3781 . . . . . . . 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 1163 . . . . . 6  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )
17 suceq 4780 . . . . . . . . 9  |-  ( m  =  (/)  ->  suc  m  =  suc  (/) )
1817feq2d 5544 . . . . . . . 8  |-  ( m  =  (/)  ->  ( {
<. (/) ,  C >. } : suc  m --> A  <->  { <. (/) ,  C >. } : suc  (/) --> A ) )
19 raleq 2915 . . . . . . . 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 1286 . . . . . . 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 3070 . . . . . 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 658 . . . . 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 4530 . . . . . 6  |-  { <. (/)
,  C >. }  e.  _V
2623, 24, 25axdc3lem3 8617 . . . . 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 212 . . . 4  |-  ( C  e.  A  ->  { <. (/)
,  C >. }  e.  S )
28 ne0i 3640 . . . 4  |-  ( {
<. (/) ,  C >. }  e.  S  ->  S  =/=  (/) )
2927, 28syl 16 . . 3  |-  ( C  e.  A  ->  S  =/=  (/) )
30 ssrab2 3434 . . . . . . 7  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S
3123, 24axdc3lem 8615 . . . . . . . 8  |-  S  e. 
_V
3231elpw2 4453 . . . . . . 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 209 . . . . . 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 2973 . . . . . . . . . 10  |-  x  e. 
_V
3623, 24, 35axdc3lem3 8617 . . . . . . . . 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 984 . . . . . . . . . . . . . . . 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 2973 . . . . . . . . . . . . . . . . . . . . . 22  |-  m  e. 
_V
3938sucid 4794 . . . . . . . . . . . . . . . . . . . . 21  |-  m  e. 
suc  m
40 ffvelrn 5838 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x : suc  m --> A  /\  m  e.  suc  m )  ->  (
x `  m )  e.  A )
4139, 40mpan2 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : suc  m --> A  -> 
( x `  m
)  e.  A )
42 ffvelrn 5838 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( x `
 m )  e.  A )  ->  ( F `  ( x `  m ) )  e.  ( ~P A  \  { (/) } ) )
4341, 42sylan2 471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( F `  ( x `  m
) )  e.  ( ~P A  \  { (/)
} ) )
44 eldifn 3476 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  -.  ( F `  (
x `  m )
)  e.  { (/) } )
45 fvex 5698 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( x `  m ) )  e. 
_V
4645elsnc 3898 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( x `
 m ) )  e.  { (/) }  <->  ( F `  ( x `  m
) )  =  (/) )
4746necon3bbii 2637 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <-> 
( F `  (
x `  m )
)  =/=  (/) )
48 n0 3643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  ( x `
 m ) )  =/=  (/)  <->  E. z  z  e.  ( F `  (
x `  m )
) )
4947, 48bitri 249 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5044, 49sylib 196 . . . . . . . . . . . . . . . . . . 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 1020 . . . . . . . . . . . . . . . . . . . . . . . 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 3475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  -> 
( F `  (
x `  m )
)  e.  ~P A
)
54 elelpwi 3868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( F `  ( x `
 m ) )  e.  ~P A )  ->  z  e.  A
)
5554expcom 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ~P A  -> 
( z  e.  ( F `  ( x `
 m ) )  ->  z  e.  A
) )
5643, 53, 553syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  z  e.  A ) )
57 peano2 6495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  om  ->  suc  m  e.  om )
58573ad2ant3 1006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  suc  m  e.  om )
59583ad2ant1 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  x : suc  m --> A )
6135dmex 6510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  dom  x  e.  _V
62 vex 2973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  z  e. 
_V
63 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  { <. dom  x ,  z >. }  =  { <. dom  x ,  z >. }
64 fsng 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  ( { <. dom  x ,  z >. } : { dom  x } --> { z }  <->  { <. dom  x , 
z >. }  =  { <. dom  x ,  z
>. } ) )
6563, 64mpbiri 233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  { <. dom  x , 
z >. } : { dom  x } --> { z } )
6661, 62, 65mp2an 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  { <. dom  x ,  z >. } : { dom  x }
--> { z }
67 simpr 458 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  z  e.  A )
6867snssd 4015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { z }  C_  A )
69 fss 5564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( { <. dom  x , 
z >. } : { dom  x } --> { z }  /\  { z }  C_  A )  ->  { <. dom  x , 
z >. } : { dom  x } --> A )
7066, 68, 69sylancr 658 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { <. dom  x ,  z >. } : { dom  x }
--> A )
71 fdm 5560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  dom  x  =  suc  m
)
7257adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  suc  m  e. 
om )
73 eleq1 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
om 
<->  suc  m  e.  om ) )
7473adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  om  <->  suc  m  e. 
om ) )
7572, 74mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  dom  x  e. 
om )
76 nnord 6483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  e.  om  ->  Ord 
dom  x )
77 ordirr 4733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( Ord 
dom  x  ->  -.  dom  x  e.  dom  x
)
7875, 76, 773syl 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  dom  x )
79 eleq2 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
dom  x  <->  dom  x  e. 
suc  m ) )
8079adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  dom  x  <->  dom  x  e. 
suc  m ) )
8178, 80mtbid 300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  suc  m )
82 disjsn 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( suc  m  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
suc  m )
8381, 82sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
8471, 83sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( suc  m  i^i  { dom  x }
)  =  (/) )
8584adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
86 fun2 5573 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : ( suc  m  u.  { dom  x } ) --> A )
88 sneq 3884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( dom  x  =  suc  m  ->  { dom  x }  =  { suc  m }
)
8988uneq2d 3507 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  ( suc  m  u.  { suc  m } ) )
90 df-suc 4721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  suc  suc  m  =  ( suc  m  u.  { suc  m } )
9189, 90syl6eqr 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  u.  { dom  x } )  =  suc  suc  m )
9493feq2d 5544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A )
9695ex 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  A  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
9796adantrd 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( z  e.  A  /\  (
x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) )
9897a1d 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 ) ) )
9998ancoms 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  Fun  x )
103102adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  x )
10461, 62funsn 5463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  Fun  { <. dom  x ,  z
>. }
105103, 104jctir 535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( Fun  x  /\  Fun  { <. dom  x ,  z >. } ) )
10662dmsnop 5310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  dom  { <. dom  x ,  z
>. }  =  { dom  x }
107106ineq2i 3546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  i^i  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  i^i  { dom  x } )
108 disjsn 3933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
dom  x )
10978, 108sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  { dom  x } )  =  (/) )
110107, 109syl5eq 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
11171, 110sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
112 funun 5457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( Fun  x  /\  Fun  { <. dom  x , 
z >. } )  /\  ( dom  x  i^i  dom  {
<. dom  x ,  z
>. } )  =  (/) )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
113105, 111, 112syl2anc 656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
114 ssun1 3516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  om  ->  Ord  m )
117 0elsuc 6445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( Ord  m  ->  (/)  e.  suc  m )
118116, 117syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  om  ->  (/)  e.  suc  m )
119118adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  suc  m
)
12071eleq2d 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( (/)  e.  dom  x  <->  (/)  e.  suc  m ) )
121120adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( (/)  e.  dom  x 
<->  (/)  e.  suc  m ) )
122119, 121mpbird 232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  dom  x
)
123 funssfv 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 (/) )  =  ( x `  (/) ) )
125124eqeq1d 2449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
126125ancoms 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
1271263adant1 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )
132 nfv 1678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  x : suc  m --> A
133 nfv 1678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  m  e.  om
134131, 132, 133nf3an 1867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )
135 nfv 1678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k  z  e.  ( F `
 ( x `  m ) )
136 nfv 1678 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( z  e.  A  /\  ( x `  (/) )  =  C )
137134, 135, 136nf3an 1867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  suc  m  -> 
( k  e.  m  \/  k  =  m
) )
140 rsp 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
k  e.  m  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) ) )
141140impcom 430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( k  e.  m  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
142141ad2ant2lr 742 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  m )  ->  suc  k  e.  suc  m )
149 eleq2 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  m  ->  ( suc  k  e. 
dom  x  <->  suc  k  e. 
suc  m ) )
150149biimparc 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( suc  k  e.  suc  m  /\  dom  x  =  suc  m )  ->  suc  k  e.  dom  x )
151148, 71, 150syl2an 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  suc  k  e.  dom  x )
152 funssfv 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1541533adant2 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( dom  x  =  suc  m  ->  ( k  e.  dom  x 
<->  k  e.  suc  m
) )
158157biimparc 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  e.  suc  m  /\  dom  x  =  suc  m )  ->  k  e.  dom  x )
15971, 158sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
1601593adant1 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
161 funssfv 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
1631623adant1r 1206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
164163fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) )
168167a1d 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
) ) ) )
1691683expib 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1001 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
172 ssun2 3517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( k  =  m  ->  suc  k  =  suc  m )
175174eqeq2d 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( k  =  m  ->  ( dom  x  =  suc  k  <->  dom  x  =  suc  m
) )
176175biimpar 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  dom  x  =  suc  k )
17761snid 3902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  dom  x  e.  { dom  x }
178177, 106eleqtrri 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  dom  x  e.  dom  { <. dom  x ,  z >. }
179176, 178syl6eqelr 2530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  suc  k  e. 
dom  { <. dom  x , 
z >. } )
18071, 179sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
1811803adant2 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
182 funssfv 5702 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  ( { <. dom  x ,  z >. } `  suc  k ) )
1841763adant2 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  dom  x  =  suc  k )
18561, 62fvsn 5908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( {
<. dom  x ,  z
>. } `  dom  x
)  =  z
186 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  dom  x )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
187185, 186syl5reqr 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
190183, 189eqtrd 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  z )
1911903expa 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1921913adant2 1002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1931623adant1l 1205 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
194 fveq2 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( k  =  m  ->  (
x `  k )  =  ( x `  m ) )
195194adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( x `  k
)  =  ( x `
 m ) )
1961953ad2ant1 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
x `  k )  =  ( x `  m ) )
197193, 196eqtrd 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 m ) )
198197fveq2d 5692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) ) )
2022013expib 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) ) ) ) )
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 434 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 431 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) ) )
2132123adant3 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4780 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( p  =  suc  m  ->  suc  p  =  suc  suc  m )
216215feq2d 5544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  <->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
217 raleq 2915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3070 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4530 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  e.  _V
22235, 221unex 6377 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  u.  { <. dom  x ,  z >. } )  e.  _V
22323, 24, 222axdc3lem3 8617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
)
2252243coml 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) ) )
2292283impd 1196 . . . . . . . . . . . . . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . . . . . . . . . . . . . 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 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
) ) )
23252, 231mpdi 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 ) )
233232imp 429 . . . . . . . . . . . . . . . . . . . . . 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 5122 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x ) )
235 frel 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x : suc  m --> A  ->  Rel  x )
236 resdm 5145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Rel  x  ->  ( x  |` 
dom  x )  =  x )
237235, 236syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x : suc  m --> A  -> 
( x  |`  dom  x
)  =  x )
238237adantl 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( x  |`  dom  x )  =  x )
23971, 75sylan2 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { dom  x }  i^i  dom  x )  =  ( dom  x  i^i  { dom  x } )
242241eqeq1i 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( dom  x  i^i 
{ dom  x }
)  =  (/) )
24361, 62fnsn 5468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  Fn  { dom  x }
244 fnresdisj 5518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( {
<. dom  x ,  z
>. }  Fn  { dom  x }  ->  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) ) )
245243, 244ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
246242, 245, 1083bitr3ri 276 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -. 
dom  x  e.  dom  x 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
247240, 246sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  ( x  u.  (/) ) )
250 un0 3659 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  u.  (/) )  =  x
251249, 250syl6eq 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  x )
252234, 251syl5eq 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
253252ancoms 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
2542533adant1 1001 . . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . . . . . . . . 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 463 . . . . . . . . . . . . . . . . . . . . . . 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 3504 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  x  u.  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  u.  { dom  x } )
258 dmun 5042 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  ( dom  x  u.  dom  {
<. dom  x ,  z
>. } )
259 df-suc 4721 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  dom  x  =  ( dom  x  u.  { dom  x } )
260257, 258, 2593eqtr4i 2471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
261256, 260jctil 534 . . . . . . . . . . . . . . . . . . . . . 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 5036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  ->  dom  y  =  dom  ( x  u.  { <. dom  x ,  z >. } ) )
263262eqeq1d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( dom  y  =  suc  dom  x  <->  dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
) )
264 reseq1 5100 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( y  |`  dom  x
)  =  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
) )
265264eqeq1d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( y  |`  dom  x )  =  x  <-> 
( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )
266263, 265anbi12d 705 . . . . . . . . . . . . . . . . . . . . . . 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 3070 . . . . . . . . . . . . . . . . . . . . . 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 656 . . . . . . . . . . . . . . . . . . . . 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 1200 . . . . . . . . . . . . . . . . . . . 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 1695 . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . 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 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 ) ) ) )
27437, 273mpan2d 669 . . . . . . . . . . . . . . 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 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 ) ) ) )
2762753expd 1199 . . . . . . . . . . . . 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 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 ) ) ) ) ) )
2782773imp 1176 . . . . . . . . . . 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 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 ) ) ) )
280279rexlimiv 2833 . . . . . . . . 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 195 . . . . . . . 8  |-  ( x  e.  S  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) )
282281impcom 430 . . . . . . 7  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
283 rabn0 3654 . . . . . . 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 212 . . . . . 6  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =/=  (/) )
28531rabex 4440 . . . . . . . 8  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  _V
286285elsnc 3898 . . . . . . 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 2637 . . . . . 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 212 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  -.  { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) } )
28934, 288eldifd 3336 . . . 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 5864 . . 3  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  G : S
--> ( ~P S  \  { (/) } ) )
29231axdc2 8614 . . 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 474 . 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 8616 . 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364   E.wex 1591    e. wcel 1761   {cab 2427    =/= wne 2604   A.wral 2713   E.wrex 2714   {crab 2717   _Vcvv 2970    \ cdif 3322    u. cun 3323    i^i cin 3324    C_ wss 3325   (/)c0 3634   ~Pcpw 3857   {csn 3874   <.cop 3880    e. cmpt 4347   Ord word 4714   suc csuc 4717   dom cdm 4836    |` cres 4838   Rel wrel 4841   Fun wfun 5409    Fn wfn 5410   -->wf 5411   ` cfv 5415   omcom 6475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-dc 8611
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-om 6476  df-1o 6916
This theorem is referenced by:  axdc3  8619
  Copyright terms: Public domain W3C validator