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

Theorem axdc3lem4 8095
Description: Lemma for axdc3 8096. 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 8088 (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 8088 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 8091. See axdc3lem2 8093 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 4691 . . . . . 6  |-  (/)  e.  om
2 eqid 2296 . . . . . . . . . 10  |-  { <. (/)
,  C >. }  =  { <. (/) ,  C >. }
3 fsng 5713 . . . . . . . . . . 11  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
41, 3mpan 651 . . . . . . . . . 10  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : { (/) } --> { C } 
<->  { <. (/) ,  C >. }  =  { <. (/) ,  C >. } ) )
52, 4mpbiri 224 . . . . . . . . 9  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> { C } )
6 snssi 3775 . . . . . . . . 9  |-  ( C  e.  A  ->  { C }  C_  A )
7 fss 5413 . . . . . . . . 9  |-  ( ( { <. (/) ,  C >. } : { (/) } --> { C }  /\  { C }  C_  A )  ->  { <. (/)
,  C >. } : { (/) } --> A )
85, 6, 7syl2anc 642 . . . . . . . 8  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : { (/) } --> A )
9 suc0 4482 . . . . . . . . 9  |-  suc  (/)  =  { (/)
}
109feq2i 5400 . . . . . . . 8  |-  ( {
<. (/) ,  C >. } : suc  (/) --> A  <->  { <. (/) ,  C >. } : { (/) } --> A )
118, 10sylibr 203 . . . . . . 7  |-  ( C  e.  A  ->  { <. (/)
,  C >. } : suc  (/) --> A )
12 fvsng 5730 . . . . . . . 8  |-  ( (
(/)  e.  om  /\  C  e.  A )  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
131, 12mpan 651 . . . . . . 7  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } `
 (/) )  =  C )
14 ral0 3571 . . . . . . . 8  |-  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) )
1514a1i 10 . . . . . . 7  |-  ( C  e.  A  ->  A. k  e.  (/)  ( { <. (/)
,  C >. } `  suc  k )  e.  ( F `  ( {
<. (/) ,  C >. } `
 k ) ) )
1611, 13, 153jca 1132 . . . . . 6  |-  ( C  e.  A  ->  ( { <. (/) ,  C >. } : suc  (/) --> A  /\  ( { <. (/) ,  C >. } `
 (/) )  =  C  /\  A. k  e.  (/)  ( { <. (/) ,  C >. } `  suc  k
)  e.  ( F `
 ( { <. (/)
,  C >. } `  k ) ) ) )
17 suceq 4473 . . . . . . . . 9  |-  ( m  =  (/)  ->  suc  m  =  suc  (/) )
1817feq2d 5396 . . . . . . . 8  |-  ( m  =  (/)  ->  ( {
<. (/) ,  C >. } : suc  m --> A  <->  { <. (/) ,  C >. } : suc  (/) --> A ) )
19 raleq 2749 . . . . . . . 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 1254 . . . . . . 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 2897 . . . . . 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 644 . . . . 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 4232 . . . . . 6  |-  { <. (/)
,  C >. }  e.  _V
2623, 24, 25axdc3lem3 8094 . . . . 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 203 . . . 4  |-  ( C  e.  A  ->  { <. (/)
,  C >. }  e.  S )
28 ne0i 3474 . . . 4  |-  ( {
<. (/) ,  C >. }  e.  S  ->  S  =/=  (/) )
2927, 28syl 15 . . 3  |-  ( C  e.  A  ->  S  =/=  (/) )
30 ssrab2 3271 . . . . . . 7  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  C_  S
3123, 24axdc3lem 8092 . . . . . . . 8  |-  S  e. 
_V
3231elpw2 4191 . . . . . . 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 200 . . . . . 6  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ~P S
3433a1i 10 . . . . 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 2804 . . . . . . . . . 10  |-  x  e. 
_V
3623, 24, 35axdc3lem3 8094 . . . . . . . . 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 956 . . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . . . . . . . . . 22  |-  m  e. 
_V
3938sucid 4487 . . . . . . . . . . . . . . . . . . . . 21  |-  m  e. 
suc  m
40 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x : suc  m --> A  /\  m  e.  suc  m )  ->  (
x `  m )  e.  A )
4139, 40mpan2 652 . . . . . . . . . . . . . . . . . . . 20  |-  ( x : suc  m --> A  -> 
( x `  m
)  e.  A )
42 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  ( x `
 m )  e.  A )  ->  ( F `  ( x `  m ) )  e.  ( ~P A  \  { (/) } ) )
4341, 42sylan2 460 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( F `  ( x `  m
) )  e.  ( ~P A  \  { (/)
} ) )
44 eldifn 3312 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  -.  ( F `  (
x `  m )
)  e.  { (/) } )
45 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( F `
 ( x `  m ) )  e. 
_V
4645elsnc 3676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  ( x `
 m ) )  e.  { (/) }  <->  ( F `  ( x `  m
) )  =  (/) )
4746necon3bbii 2490 . . . . . . . . . . . . . . . . . . . . 21  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <-> 
( F `  (
x `  m )
)  =/=  (/) )
48 n0 3477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  ( x `
 m ) )  =/=  (/)  <->  E. z  z  e.  ( F `  (
x `  m )
) )
4947, 48bitri 240 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( F `  (
x `  m )
)  e.  { (/) }  <->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5044, 49sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  ->  E. z  z  e.  ( F `  ( x `
 m ) ) )
5143, 50syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  E. z  z  e.  ( F `  (
x `  m )
) )
52 simp32 992 . . . . . . . . . . . . . . . . . . . . . . . 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 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ( ~P A  \  { (/) } )  -> 
( F `  (
x `  m )
)  e.  ~P A
)
54 elelpwi 3648 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( z  e.  ( F `
 ( x `  m ) )  /\  ( F `  ( x `
 m ) )  e.  ~P A )  ->  z  e.  A
)
5554expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( F `  ( x `
 m ) )  e.  ~P A  -> 
( z  e.  ( F `  ( x `
 m ) )  ->  z  e.  A
) )
5643, 53, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x : suc  m --> A )  ->  ( z  e.  ( F `  (
x `  m )
)  ->  z  e.  A ) )
57 peano2 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( m  e.  om  ->  suc  m  e.  om )
58573ad2ant3 978 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )  ->  suc  m  e.  om )
59583ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  x : suc  m --> A )
6135dmex 4957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  dom  x  e.  _V
62 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  z  e. 
_V
63 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  { <. dom  x ,  z >. }  =  { <. dom  x ,  z >. }
64 fsng 5713 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  ( { <. dom  x ,  z >. } : { dom  x } --> { z }  <->  { <. dom  x , 
z >. }  =  { <. dom  x ,  z
>. } ) )
6563, 64mpbiri 224 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( dom  x  e.  _V  /\  z  e.  _V )  ->  { <. dom  x , 
z >. } : { dom  x } --> { z } )
6661, 62, 65mp2an 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  { <. dom  x ,  z >. } : { dom  x }
--> { z }
67 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  z  e.  A )
6867snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { z }  C_  A )
69 fss 5413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( { <. dom  x , 
z >. } : { dom  x } --> { z }  /\  { z }  C_  A )  ->  { <. dom  x , 
z >. } : { dom  x } --> A )
7066, 68, 69sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  { <. dom  x ,  z >. } : { dom  x }
--> A )
71 fdm 5409 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  dom  x  =  suc  m
)
7257adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  suc  m  e. 
om )
73 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
om 
<->  suc  m  e.  om ) )
7473adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  om  <->  suc  m  e. 
om ) )
7572, 74mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  dom  x  e. 
om )
76 nnord 4680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  e.  om  ->  Ord 
dom  x )
77 ordirr 4426 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( Ord 
dom  x  ->  -.  dom  x  e.  dom  x
)
7875, 76, 773syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  dom  x )
79 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( dom  x  =  suc  m  ->  ( dom  x  e. 
dom  x  <->  dom  x  e. 
suc  m ) )
8079adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  e.  dom  x  <->  dom  x  e. 
suc  m ) )
8178, 80mtbid 291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  -.  dom  x  e.  suc  m )
82 disjsn 3706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( suc  m  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
suc  m )
8381, 82sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
8471, 83sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( suc  m  i^i  { dom  x }
)  =  (/) )
8584adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  i^i  { dom  x } )  =  (/) )
86 fun2 5422 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : ( suc  m  u.  { dom  x } ) --> A )
88 sneq 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( dom  x  =  suc  m  ->  { dom  x }  =  { suc  m }
)
8988uneq2d 3342 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  ( suc  m  u.  { suc  m } ) )
90 df-suc 4414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  suc  suc  m  =  ( suc  m  u.  { suc  m } )
9189, 90syl6eqr 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  =  suc  m  ->  ( suc  m  u. 
{ dom  x }
)  =  suc  suc  m )
9271, 91syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( suc  m  u.  { dom  x } )  =  suc  suc  m
)
9392ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  ( suc  m  u.  { dom  x } )  =  suc  suc  m )
9493feq2d 5396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( m  e.  om  /\  x : suc  m --> A )  /\  z  e.  A )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A )
9695ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( z  e.  A  ->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
9796adantrd 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( z  e.  A  /\  (
x `  (/) )  =  C )  ->  (
x  u.  { <. dom  x ,  z >. } ) : suc  suc  m --> A ) )
9897a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( x : suc  m --> A  ->  Fun  x )
103102adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  x )
10461, 62funsn 5316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  Fun  { <. dom  x ,  z
>. }
105103, 104jctir 524 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( Fun  x  /\  Fun  { <. dom  x ,  z >. } ) )
10662dmsnop 5163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  dom  { <. dom  x ,  z
>. }  =  { dom  x }
107106ineq2i 3380 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( dom  x  i^i  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  i^i  { dom  x } )
108 disjsn 3706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( dom  x  i^i  { dom  x } )  =  (/) 
<->  -.  dom  x  e. 
dom  x )
10978, 108sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  { dom  x } )  =  (/) )
110107, 109syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( m  e.  om  /\  dom  x  =  suc  m
)  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
11171, 110sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( dom  x  i^i  dom  { <. dom  x ,  z >. } )  =  (/) )
112 funun 5312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( Fun  x  /\  Fun  { <. dom  x , 
z >. } )  /\  ( dom  x  i^i  dom  {
<. dom  x ,  z
>. } )  =  (/) )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
113105, 111, 112syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
114 ssun1 3351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  x  C_  ( x  u.  { <. dom  x ,  z >. } )
115114a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
116 nnord 4680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( m  e.  om  ->  Ord  m )
117 0elsuc 4642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( Ord  m  ->  (/)  e.  suc  m )
118116, 117syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( m  e.  om  ->  (/)  e.  suc  m )
119118adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  suc  m
)
12071eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( x : suc  m --> A  -> 
( (/)  e.  dom  x  <->  (/)  e.  suc  m ) )
121120adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( (/)  e.  dom  x 
<->  (/)  e.  suc  m ) )
122119, 121mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  (/)  e.  dom  x
)
123 funssfv 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 (/) )  =  ( x `  (/) ) )
125124eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
126125ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( ( x  u.  { <. dom  x ,  z >. } ) `  (/) )  =  C  <->  ( x `  (/) )  =  C ) )
1271263adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )
132 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  x : suc  m --> A
133 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ k  m  e.  om
134131, 132, 133nf3an 1786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( A. k  e.  m  ( x `  suc  k )  e.  ( F `  ( x `
 k ) )  /\  x : suc  m
--> A  /\  m  e. 
om )
135 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k  z  e.  ( F `
 ( x `  m ) )
136 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ k ( z  e.  A  /\  ( x `  (/) )  =  C )
137134, 135, 136nf3an 1786 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( k  e.  suc  m  -> 
( k  e.  m  \/  k  =  m
) )
140 rsp 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( A. k  e.  m  (
x `  suc  k )  e.  ( F `  ( x `  k
) )  ->  (
k  e.  m  -> 
( x `  suc  k )  e.  ( F `  ( x `
 k ) ) ) )
141140impcom 419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( k  e.  m  /\  A. k  e.  m  ( x `  suc  k
)  e.  ( F `
 ( x `  k ) ) )  ->  ( x `  suc  k )  e.  ( F `  ( x `
 k ) ) )
142141ad2ant2lr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  Fun  ( x  u.  { <. dom  x ,  z >. } ) )
145114a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  x  C_  ( x  u.  { <. dom  x ,  z
>. } ) )
146 ordsucelsuc 4629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( Ord  m  ->  ( k  e.  m  <->  suc  k  e.  suc  m ) )
147116, 146syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( m  e.  om  ->  (
k  e.  m  <->  suc  k  e. 
suc  m ) )
148147biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  m )  ->  suc  k  e.  suc  m )
149 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  m  ->  ( suc  k  e. 
dom  x  <->  suc  k  e. 
suc  m ) )
150149biimparc 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( suc  k  e.  suc  m  /\  dom  x  =  suc  m )  ->  suc  k  e.  dom  x )
151148, 71, 150syl2an 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  suc  k  e.  dom  x )
152 funssfv 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  ( x `  suc  k
) )
1541533adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
156114a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  x  C_  (
x  u.  { <. dom  x ,  z >. } ) )
157 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( dom  x  =  suc  m  ->  ( k  e.  dom  x 
<->  k  e.  suc  m
) )
158157biimparc 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  e.  suc  m  /\  dom  x  =  suc  m )  ->  k  e.  dom  x )
15971, 158sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
1601593adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  k  e.  dom  x )
161 funssfv 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( m  e.  om  /\  k  e.  suc  m  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 k )  =  ( x `  k
) )
1631623adant1r 1175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( m  e.  om  /\  k  e.  m )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
164163fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  Fun  ( x  u.  { <. dom  x , 
z >. } ) )
172 ssun2 3352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  { <. dom  x ,  z >. }  C_  ( x  u. 
{ <. dom  x , 
z >. } )
173172a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  { <. dom  x ,  z >. }  C_  ( x  u.  { <. dom  x ,  z >. } ) )
174 suceq 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58  |-  ( k  =  m  ->  suc  k  =  suc  m )
175174eqeq2d 2307 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  ( k  =  m  ->  ( dom  x  =  suc  k  <->  dom  x  =  suc  m
) )
176175biimpar 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  dom  x  =  suc  k )
17761snid 3680 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57  |-  dom  x  e.  { dom  x }
178177, 106eleqtrri 2369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56  |-  dom  x  e.  dom  { <. dom  x ,  z >. }
179176, 178syl6eqelr 2385 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( ( k  =  m  /\  dom  x  =  suc  m
)  ->  suc  k  e. 
dom  { <. dom  x , 
z >. } )
18071, 179sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
1811803adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  suc  k  e.  dom  { <. dom  x , 
z >. } )
182 funssfv 5559 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  ( { <. dom  x ,  z >. } `  suc  k ) )
1841763adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  dom  x  =  suc  k )
18561, 62fvsn 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( {
<. dom  x ,  z
>. } `  dom  x
)  =  z
186 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  dom  x )  =  ( { <. dom  x , 
z >. } `  suc  k ) )
187185, 186syl5reqr 2343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54  |-  ( dom  x  =  suc  k  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
188184, 187syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( ( k  =  m  /\  m  e.  om  /\  dom  x  =  suc  m )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
18971, 188syl3an3 1217 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. } `  suc  k )  =  z )
190183, 189eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( k  =  m  /\  m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } ) `
 suc  k )  =  z )
1911903expa 1151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1921913adant2 974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  suc  k )  =  z )
1931623adant1l 1174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 k ) )
194 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  ( k  =  m  ->  (
x `  k )  =  ( x `  m ) )
195194adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( ( k  =  m  /\  m  e.  om )  ->  ( x `  k
)  =  ( x `
 m ) )
1961953ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
x `  k )  =  ( x `  m ) )
197193, 196eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( ( ( k  =  m  /\  m  e.  om )  /\  k  e.  suc  m  /\  x : suc  m
--> A )  ->  (
( x  u.  { <. dom  x ,  z
>. } ) `  k
)  =  ( x `
 m ) )
198197fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2364 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1154 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 368 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 73 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 420 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( p  =  suc  m  ->  suc  p  =  suc  suc  m )
216215feq2d 5396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( p  =  suc  m  -> 
( ( x  u. 
{ <. dom  x , 
z >. } ) : suc  p --> A  <->  ( x  u.  { <. dom  x , 
z >. } ) : suc  suc  m --> A ) )
217 raleq 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  e.  _V
22235, 221unex 4534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  u.  { <. dom  x ,  z >. } )  e.  _V
22323, 24, 222axdc3lem3 8094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1165 . . . . . . . . . . . . . . . . . . . . . . . . . 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 423 . . . . . . . . . . . . . . . . . . . . . . . . 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 72 . . . . . . . . . . . . . . . . . . . . . . . 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 38 . . . . . . . . . . . . . . . . . . . . . . 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 418 . . . . . . . . . . . . . . . . . . . . . 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 4986 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
)  =  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x ) )
235 frel 5408 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x : suc  m --> A  ->  Rel  x )
236 resdm 5009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( Rel  x  ->  ( x  |` 
dom  x )  =  x )
237235, 236syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x : suc  m --> A  -> 
( x  |`  dom  x
)  =  x )
238237adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( x  |`  dom  x )  =  x )
23971, 75sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  dom  x  e.  om )
24076, 77syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( dom  x  e.  om  ->  -. 
dom  x  e.  dom  x )
241 incom 3374 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( { dom  x }  i^i  dom  x )  =  ( dom  x  i^i  { dom  x } )
242241eqeq1i 2303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( { dom  x }  i^i  dom  x )  =  (/) 
<->  ( dom  x  i^i 
{ dom  x }
)  =  (/) )
24361, 62fnsn 5320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { <. dom  x ,  z >. }  Fn  { dom  x }
244 fnresdisj 5370 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 267 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( -. 
dom  x  e.  dom  x 
<->  ( { <. dom  x ,  z >. }  |`  dom  x
)  =  (/) )
247240, 246sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( dom  x  e.  om  ->  ( { <. dom  x , 
z >. }  |`  dom  x
)  =  (/) )
248239, 247syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( { <. dom  x ,  z >. }  |`  dom  x )  =  (/) )
249238, 248uneq12d 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  ( x  u.  (/) ) )
250 un0 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  u.  (/) )  =  x
251249, 250syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  |`  dom  x )  u.  ( { <. dom  x ,  z >. }  |`  dom  x
) )  =  x )
252234, 251syl5eq 2340 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( m  e.  om  /\  x : suc  m --> A )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
253252ancoms 439 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x : suc  m --> A  /\  m  e.  om )  ->  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x )  =  x )
2542533adant1 973 . . . . . . . . . . . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . . 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 3339 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( dom  x  u.  dom  { <. dom  x ,  z
>. } )  =  ( dom  x  u.  { dom  x } )
258 dmun 4901 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  ( dom  x  u.  dom  {
<. dom  x ,  z
>. } )
259 df-suc 4414 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  suc  dom  x  =  ( dom  x  u.  { dom  x } )
260257, 258, 2593eqtr4i 2326 . . . . . . . . . . . . . . . . . . . . . . 23  |-  dom  (
x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
261256, 260jctil 523 . . . . . . . . . . . . . . . . . . . . . 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 4895 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  ->  dom  y  =  dom  ( x  u.  { <. dom  x ,  z >. } ) )
263262eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( dom  y  =  suc  dom  x  <->  dom  ( x  u.  { <. dom  x ,  z >. } )  =  suc  dom  x
) )
264 reseq1 4965 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( y  |`  dom  x
)  =  ( ( x  u.  { <. dom  x ,  z >. } )  |`  dom  x
) )
265264eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  ( x  u. 
{ <. dom  x , 
z >. } )  -> 
( ( y  |`  dom  x )  =  x  <-> 
( ( x  u. 
{ <. dom  x , 
z >. } )  |`  dom  x )  =  x ) )
266263, 265anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . . . . . . . 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 1169 . . . . . . . . . . . . . . . . . . . 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 1626 . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . 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 14 . . . . . . . . . . . . . . . . 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 73 . . . . . . . . . . . . . . . 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 655 . . . . . . . . . . . . . . 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 73 . . . . . . . . . . . . . 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 1168 . . . . . . . . . . . . 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 73 . . . . . . . . . . . 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 1145 . . . . . . . . . . 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 27 . . . . . . . . . 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 2674 . . . . . . . . 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 187 . . . . . . . 8  |-  ( x  e.  S  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) ) )
282281impcom 419 . . . . . . 7  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  E. y  e.  S  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) )
283 rabn0 3487 . . . . . . 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 203 . . . . . 6  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  =/=  (/) )
28531rabex 4181 . . . . . . . 8  |-  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  _V
286285elsnc 3676 . . . . . . 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 2490 . . . . . 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 203 . . . . 5  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  -.  { y  e.  S  | 
( dom  y  =  suc  dom  x  /\  (
y  |`  dom  x )  =  x ) }  e.  { (/) } )
289 eldif 3175 . . . . 5  |-  ( { 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 ) }  e.  ~P S  /\  -.  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) }  e.  { (/) } ) )
29034, 288, 289sylanbrc 645 . . . 4  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  S )  ->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x )  =  x ) }  e.  ( ~P S  \  { (/)
} ) )
291 axdc3lem4.3 . . . 4  |-  G  =  ( x  e.  S  |->  { y  e.  S  |  ( dom  y  =  suc  dom  x  /\  ( y  |`  dom  x
)  =  x ) } )
292290, 291fmptd 5700 . . 3  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  G : S
--> ( ~P S  \  { (/) } ) )
29331axdc2 8091 . . 3  |-  ( ( S  =/=  (/)  /\  G : S --> ( ~P S  \  { (/) } ) )  ->  E. h ( h : om --> S  /\  A. k  e.  om  (
h `  suc  k )  e.  ( G `  ( h `  k
) ) ) )
29429, 292, 293syl2an 463 . 2  |-  ( ( C  e.  A  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. h
( h : om --> S  /\  A. k  e. 
om  ( h `  suc  k )  e.  ( G `  ( h `
 k ) ) ) )
29523, 24, 291axdc3lem2 8093 . 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 ) ) ) )
296294, 295syl 15 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 176    \/ wo 357    /\ wa 358    /\ w3a 934   E.wex 1531    = wceq 1632    e. wcel 1696   {cab 2282    =/= wne 2459   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    \ cdif 3162    u. cun 3163    i^i cin 3164    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   {csn 3653   <.cop 3656    e. cmpt 4093   Ord word 4407   suc csuc 4410   omcom 4672   dom cdm 4705    |` cres 4707   Rel wrel 4710   Fun wfun 5265    Fn wfn 5266   -->wf 5267   ` cfv 5271
This theorem is referenced by:  axdc3  8096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-dc 8088
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-1o 6495
  Copyright terms: Public domain W3C validator