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

Theorem axdc2lem 8074
Description: Lemma for axdc2 8075. We construct a relation  R based on  F such that  x R y iff  y  e.  ( F `
 x ), and show that the "function" described by ax-dc 8072 can be restricted so that it is a real function (since the stated properties only show that it is the superset of a function). (Contributed by Mario Carneiro, 25-Jan-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
axdc2lem.1  |-  A  e. 
_V
axdc2lem.2  |-  R  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }
axdc2lem.3  |-  G  =  ( x  e.  om  |->  ( h `  x
) )
Assertion
Ref Expression
axdc2lem  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. g ( g : om --> A  /\  A. k  e.  om  (
g `  suc  k )  e.  ( F `  ( g `  k
) ) ) )
Distinct variable groups:    A, g, h    x, A, y, h   
g, F, h    x, F, y    g, G, k   
x, G, y, k    R, h, k, x
Allowed substitution hints:    A( k)    R( y, g)    F( k)    G( h)

Proof of Theorem axdc2lem
Dummy variable  r is distinct from all other variables.
StepHypRef Expression
1 ffvelrn 5663 . . . . . . . . 9  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  ( F `  x )  e.  ( ~P A  \  { (/) } ) )
2 eldifsni 3750 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  -> 
( F `  x
)  =/=  (/) )
3 n0 3464 . . . . . . . . . 10  |-  ( ( F `  x )  =/=  (/)  <->  E. y  y  e.  ( F `  x
) )
42, 3sylib 188 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  ->  E. y  y  e.  ( F `  x ) )
51, 4syl 15 . . . . . . . 8  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  E. y 
y  e.  ( F `
 x ) )
65ralrimiva 2626 . . . . . . 7  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  A. x  e.  A  E. y 
y  e.  ( F `
 x ) )
7 rabid2 2717 . . . . . . 7  |-  ( A  =  { x  e.  A  |  E. y 
y  e.  ( F `
 x ) }  <->  A. x  e.  A  E. y  y  e.  ( F `  x ) )
86, 7sylibr 203 . . . . . 6  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  A  =  { x  e.  A  |  E. y  y  e.  ( F `  x
) } )
9 axdc2lem.2 . . . . . . . 8  |-  R  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }
109dmeqi 4880 . . . . . . 7  |-  dom  R  =  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x ) ) }
11 19.42v 1846 . . . . . . . . 9  |-  ( E. y ( x  e.  A  /\  y  e.  ( F `  x
) )  <->  ( x  e.  A  /\  E. y 
y  e.  ( F `
 x ) ) )
1211abbii 2395 . . . . . . . 8  |-  { x  |  E. y ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  |  (
x  e.  A  /\  E. y  y  e.  ( F `  x ) ) }
13 dmopab 4889 . . . . . . . 8  |-  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  |  E. y ( x  e.  A  /\  y  e.  ( F `  x
) ) }
14 df-rab 2552 . . . . . . . 8  |-  { x  e.  A  |  E. y  y  e.  ( F `  x ) }  =  { x  |  ( x  e.  A  /\  E. y 
y  e.  ( F `
 x ) ) }
1512, 13, 143eqtr4i 2313 . . . . . . 7  |-  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  e.  A  |  E. y  y  e.  ( F `  x
) }
1610, 15eqtri 2303 . . . . . 6  |-  dom  R  =  { x  e.  A  |  E. y  y  e.  ( F `  x
) }
178, 16syl6reqr 2334 . . . . 5  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  dom  R  =  A )
1817neeq1d 2459 . . . 4  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( dom  R  =/=  (/)  <->  A  =/=  (/) ) )
1918biimparc 473 . . 3  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  dom  R  =/=  (/) )
20 eldifi 3298 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  -> 
( F `  x
)  e.  ~P A
)
21 elelpwi 3635 . . . . . . . . . . 11  |-  ( ( y  e.  ( F `
 x )  /\  ( F `  x )  e.  ~P A )  ->  y  e.  A
)
2221expcom 424 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ~P A  -> 
( y  e.  ( F `  x )  ->  y  e.  A
) )
231, 20, 223syl 18 . . . . . . . . 9  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  (
y  e.  ( F `
 x )  -> 
y  e.  A ) )
2423expimpd 586 . . . . . . . 8  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( (
x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
2524exlimdv 1664 . . . . . . 7  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( E. x ( x  e.  A  /\  y  e.  ( F `  x
) )  ->  y  e.  A ) )
2625alrimiv 1617 . . . . . 6  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  A. y
( E. x ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
279rneqi 4905 . . . . . . . . 9  |-  ran  R  =  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x ) ) }
28 rnopab 4924 . . . . . . . . 9  |-  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }
2927, 28eqtri 2303 . . . . . . . 8  |-  ran  R  =  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }
3029sseq1i 3202 . . . . . . 7  |-  ( ran 
R  C_  A  <->  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }  C_  A )
31 abss 3242 . . . . . . 7  |-  ( { y  |  E. x
( x  e.  A  /\  y  e.  ( F `  x )
) }  C_  A  <->  A. y ( E. x
( x  e.  A  /\  y  e.  ( F `  x )
)  ->  y  e.  A ) )
3230, 31bitri 240 . . . . . 6  |-  ( ran 
R  C_  A  <->  A. y
( E. x ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
3326, 32sylibr 203 . . . . 5  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  R  C_  A )
3433, 17sseqtr4d 3215 . . . 4  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  R  C_  dom  R )
3534adantl 452 . . 3  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  R  C_  dom  R )
36 fvrn0 5550 . . . . . . . . . 10  |-  ( F `
 x )  e.  ( ran  F  u.  {
(/) } )
37 elssuni 3855 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ( ran  F  u.  { (/) } )  -> 
( F `  x
)  C_  U. ( ran  F  u.  { (/) } ) )
3836, 37ax-mp 8 . . . . . . . . 9  |-  ( F `
 x )  C_  U. ( ran  F  u.  {
(/) } )
3938sseli 3176 . . . . . . . 8  |-  ( y  e.  ( F `  x )  ->  y  e.  U. ( ran  F  u.  { (/) } ) )
4039anim2i 552 . . . . . . 7  |-  ( ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
( x  e.  A  /\  y  e.  U. ( ran  F  u.  { (/) } ) ) )
4140ssopab2i 4292 . . . . . 6  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x ) ) } 
C_  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  U. ( ran  F  u.  { (/) } ) ) }
42 df-xp 4695 . . . . . 6  |-  ( A  X.  U. ( ran 
F  u.  { (/) } ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e. 
U. ( ran  F  u.  { (/) } ) ) }
4341, 9, 423sstr4i 3217 . . . . 5  |-  R  C_  ( A  X.  U. ( ran  F  u.  { (/) } ) )
44 axdc2lem.1 . . . . . 6  |-  A  e. 
_V
45 frn 5395 . . . . . . . . . 10  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  F  C_  ( ~P A  \  { (/)
} ) )
4645adantl 452 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  F  C_  ( ~P A  \  { (/) } ) )
4744pwex 4193 . . . . . . . . . . 11  |-  ~P A  e.  _V
48 difexg 4162 . . . . . . . . . . 11  |-  ( ~P A  e.  _V  ->  ( ~P A  \  { (/)
} )  e.  _V )
4947, 48ax-mp 8 . . . . . . . . . 10  |-  ( ~P A  \  { (/) } )  e.  _V
5049ssex 4158 . . . . . . . . 9  |-  ( ran 
F  C_  ( ~P A  \  { (/) } )  ->  ran  F  e.  _V )
5146, 50syl 15 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  F  e.  _V )
52 p0ex 4197 . . . . . . . 8  |-  { (/) }  e.  _V
53 unexg 4521 . . . . . . . 8  |-  ( ( ran  F  e.  _V  /\ 
{ (/) }  e.  _V )  ->  ( ran  F  u.  { (/) } )  e. 
_V )
5451, 52, 53sylancl 643 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ( ran  F  u.  { (/) } )  e. 
_V )
55 uniexg 4517 . . . . . . 7  |-  ( ( ran  F  u.  { (/)
} )  e.  _V  ->  U. ( ran  F  u.  { (/) } )  e. 
_V )
5654, 55syl 15 . . . . . 6  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  U. ( ran  F  u.  { (/) } )  e. 
_V )
57 xpexg 4800 . . . . . 6  |-  ( ( A  e.  _V  /\  U. ( ran  F  u.  {
(/) } )  e.  _V )  ->  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )
5844, 56, 57sylancr 644 . . . . 5  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )
59 ssexg 4160 . . . . 5  |-  ( ( R  C_  ( A  X.  U. ( ran  F  u.  { (/) } ) )  /\  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )  ->  R  e.  _V )
6043, 58, 59sylancr 644 . . . 4  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  R  e.  _V )
61 n0 3464 . . . . . . . . 9  |-  ( dom  r  =/=  (/)  <->  E. x  x  e.  dom  r )
62 vex 2791 . . . . . . . . . . 11  |-  x  e. 
_V
6362eldm 4876 . . . . . . . . . 10  |-  ( x  e.  dom  r  <->  E. y  x r y )
6463exbii 1569 . . . . . . . . 9  |-  ( E. x  x  e.  dom  r 
<->  E. x E. y  x r y )
6561, 64bitr2i 241 . . . . . . . 8  |-  ( E. x E. y  x r y  <->  dom  r  =/=  (/) )
66 dmeq 4879 . . . . . . . . 9  |-  ( r  =  R  ->  dom  r  =  dom  R )
6766neeq1d 2459 . . . . . . . 8  |-  ( r  =  R  ->  ( dom  r  =/=  (/)  <->  dom  R  =/=  (/) ) )
6865, 67syl5bb 248 . . . . . . 7  |-  ( r  =  R  ->  ( E. x E. y  x r y  <->  dom  R  =/=  (/) ) )
69 rneq 4904 . . . . . . . 8  |-  ( r  =  R  ->  ran  r  =  ran  R )
7069, 66sseq12d 3207 . . . . . . 7  |-  ( r  =  R  ->  ( ran  r  C_  dom  r  <->  ran 
R  C_  dom  R ) )
7168, 70anbi12d 691 . . . . . 6  |-  ( r  =  R  ->  (
( E. x E. y  x r y  /\  ran  r  C_  dom  r
)  <->  ( dom  R  =/=  (/)  /\  ran  R  C_ 
dom  R ) ) )
72 breq 4025 . . . . . . . 8  |-  ( r  =  R  ->  (
( h `  k
) r ( h `
 suc  k )  <->  ( h `  k ) R ( h `  suc  k ) ) )
7372ralbidv 2563 . . . . . . 7  |-  ( r  =  R  ->  ( A. k  e.  om  ( h `  k
) r ( h `
 suc  k )  <->  A. k  e.  om  (
h `  k ) R ( h `  suc  k ) ) )
7473exbidv 1612 . . . . . 6  |-  ( r  =  R  ->  ( E. h A. k  e. 
om  ( h `  k ) r ( h `  suc  k
)  <->  E. h A. k  e.  om  ( h `  k ) R ( h `  suc  k
) ) )
7571, 74imbi12d 311 . . . . 5  |-  ( r  =  R  ->  (
( ( E. x E. y  x r
y  /\  ran  r  C_  dom  r )  ->  E. h A. k  e.  om  ( h `  k
) r ( h `
 suc  k )
)  <->  ( ( dom 
R  =/=  (/)  /\  ran  R 
C_  dom  R )  ->  E. h A. k  e.  om  ( h `  k ) R ( h `  suc  k
) ) ) )
76 ax-dc 8072 . . . . 5  |-  ( ( E. x E. y  x r y  /\  ran  r  C_  dom  r
)  ->  E. h A. k  e.  om  ( h `  k
) r ( h `
 suc  k )
)
7775, 76vtoclg 2843 . . . 4  |-  ( R  e.  _V  ->  (
( dom  R  =/=  (/) 
/\  ran  R  C_  dom  R )  ->  E. h A. k  e.  om  ( h `  k
) R ( h `
 suc  k )
) )
7860, 77syl 15 . . 3  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ( ( dom 
R  =/=  (/)  /\  ran  R 
C_  dom  R )  ->  E. h A. k  e.  om  ( h `  k ) R ( h `  suc  k
) ) )
7919, 35, 78mp2and 660 . 2  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. h A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )
80 simpr 447 . 2  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  F : A --> ( ~P A  \  { (/)
} ) )
81 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
h `  k )  =  ( h `  x ) )
82 suceq 4457 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  suc  k  =  suc  x )
8382fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
h `  suc  k )  =  ( h `  suc  x ) )
8481, 83breq12d 4036 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
( h `  k
) R ( h `
 suc  k )  <->  ( h `  x ) R ( h `  suc  x ) ) )
8584rspccv 2881 . . . . . . . . . . . . 13  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  (
x  e.  om  ->  ( h `  x ) R ( h `  suc  x ) ) )
86 fvex 5539 . . . . . . . . . . . . . 14  |-  ( h `
 x )  e. 
_V
87 fvex 5539 . . . . . . . . . . . . . 14  |-  ( h `
 suc  x )  e.  _V
8886, 87breldm 4883 . . . . . . . . . . . . 13  |-  ( ( h `  x ) R ( h `  suc  x )  ->  (
h `  x )  e.  dom  R )
8985, 88syl6 29 . . . . . . . . . . . 12  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  (
x  e.  om  ->  ( h `  x )  e.  dom  R ) )
9089imp 418 . . . . . . . . . . 11  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  x  e.  om )  ->  ( h `  x )  e.  dom  R )
9190adantll 694 . . . . . . . . . 10  |-  ( ( ( dom  R  =  A  /\  A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )  /\  x  e.  om )  ->  (
h `  x )  e.  dom  R )
92 eleq2 2344 . . . . . . . . . . 11  |-  ( dom 
R  =  A  -> 
( ( h `  x )  e.  dom  R  <-> 
( h `  x
)  e.  A ) )
9392ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( dom  R  =  A  /\  A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )  /\  x  e.  om )  ->  (
( h `  x
)  e.  dom  R  <->  ( h `  x )  e.  A ) )
9491, 93mpbid 201 . . . . . . . . 9  |-  ( ( ( dom  R  =  A  /\  A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )  /\  x  e.  om )  ->  (
h `  x )  e.  A )
95 axdc2lem.3 . . . . . . . . 9  |-  G  =  ( x  e.  om  |->  ( h `  x
) )
9694, 95fmptd 5684 . . . . . . . 8  |-  ( ( dom  R  =  A  /\  A. k  e. 
om  ( h `  k ) R ( h `  suc  k
) )  ->  G : om --> A )
9796ex 423 . . . . . . 7  |-  ( dom 
R  =  A  -> 
( A. k  e. 
om  ( h `  k ) R ( h `  suc  k
)  ->  G : om
--> A ) )
9817, 97syl 15 . . . . . 6  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  G : om --> A ) )
9998impcom 419 . . . . 5  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  G : om --> A )
100 fveq2 5525 . . . . . . . . . 10  |-  ( x  =  k  ->  (
h `  x )  =  ( h `  k ) )
101 fvex 5539 . . . . . . . . . 10  |-  ( h `
 k )  e. 
_V
102100, 95, 101fvmpt 5602 . . . . . . . . 9  |-  ( k  e.  om  ->  ( G `  k )  =  ( h `  k ) )
103 peano2 4676 . . . . . . . . . 10  |-  ( k  e.  om  ->  suc  k  e.  om )
104 fvex 5539 . . . . . . . . . 10  |-  ( h `
 suc  k )  e.  _V
105 fveq2 5525 . . . . . . . . . . 11  |-  ( x  =  suc  k  -> 
( h `  x
)  =  ( h `
 suc  k )
)
106105, 95fvmptg 5600 . . . . . . . . . 10  |-  ( ( suc  k  e.  om  /\  ( h `  suc  k )  e.  _V )  ->  ( G `  suc  k )  =  ( h `  suc  k
) )
107103, 104, 106sylancl 643 . . . . . . . . 9  |-  ( k  e.  om  ->  ( G `  suc  k )  =  ( h `  suc  k ) )
108102, 107breq12d 4036 . . . . . . . 8  |-  ( k  e.  om  ->  (
( G `  k
) R ( G `
 suc  k )  <->  ( h `  k ) R ( h `  suc  k ) ) )
109 fvex 5539 . . . . . . . . . 10  |-  ( G `
 k )  e. 
_V
110 fvex 5539 . . . . . . . . . 10  |-  ( G `
 suc  k )  e.  _V
111 eleq1 2343 . . . . . . . . . . 11  |-  ( x  =  ( G `  k )  ->  (
x  e.  A  <->  ( G `  k )  e.  A
) )
112 fveq2 5525 . . . . . . . . . . . 12  |-  ( x  =  ( G `  k )  ->  ( F `  x )  =  ( F `  ( G `  k ) ) )
113112eleq2d 2350 . . . . . . . . . . 11  |-  ( x  =  ( G `  k )  ->  (
y  e.  ( F `
 x )  <->  y  e.  ( F `  ( G `
 k ) ) ) )
114111, 113anbi12d 691 . . . . . . . . . 10  |-  ( x  =  ( G `  k )  ->  (
( x  e.  A  /\  y  e.  ( F `  x )
)  <->  ( ( G `
 k )  e.  A  /\  y  e.  ( F `  ( G `  k )
) ) ) )
115 eleq1 2343 . . . . . . . . . . 11  |-  ( y  =  ( G `  suc  k )  ->  (
y  e.  ( F `
 ( G `  k ) )  <->  ( G `  suc  k )  e.  ( F `  ( G `  k )
) ) )
116115anbi2d 684 . . . . . . . . . 10  |-  ( y  =  ( G `  suc  k )  ->  (
( ( G `  k )  e.  A  /\  y  e.  ( F `  ( G `  k ) ) )  <-> 
( ( G `  k )  e.  A  /\  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) ) )
117109, 110, 114, 116, 9brab 4287 . . . . . . . . 9  |-  ( ( G `  k ) R ( G `  suc  k )  <->  ( ( G `  k )  e.  A  /\  ( G `  suc  k )  e.  ( F `  ( G `  k ) ) ) )
118117simprbi 450 . . . . . . . 8  |-  ( ( G `  k ) R ( G `  suc  k )  ->  ( G `  suc  k )  e.  ( F `  ( G `  k ) ) )
119108, 118syl6bir 220 . . . . . . 7  |-  ( k  e.  om  ->  (
( h `  k
) R ( h `
 suc  k )  ->  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) )
120119ralimia 2616 . . . . . 6  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  A. k  e.  om  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) )
121120adantr 451 . . . . 5  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  A. k  e.  om  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) )
122 fvrn0 5550 . . . . . . . . . 10  |-  ( h `
 x )  e.  ( ran  h  u. 
{ (/) } )
123122rgenw 2610 . . . . . . . . 9  |-  A. x  e.  om  ( h `  x )  e.  ( ran  h  u.  { (/)
} )
124 eqid 2283 . . . . . . . . . 10  |-  ( x  e.  om  |->  ( h `
 x ) )  =  ( x  e. 
om  |->  ( h `  x ) )
125124fmpt 5681 . . . . . . . . 9  |-  ( A. x  e.  om  (
h `  x )  e.  ( ran  h  u. 
{ (/) } )  <->  ( x  e.  om  |->  ( h `  x ) ) : om --> ( ran  h  u.  { (/) } ) )
126123, 125mpbi 199 . . . . . . . 8  |-  ( x  e.  om  |->  ( h `
 x ) ) : om --> ( ran  h  u.  { (/) } )
127 dcomex 8073 . . . . . . . 8  |-  om  e.  _V
128 vex 2791 . . . . . . . . . 10  |-  h  e. 
_V
129128rnex 4942 . . . . . . . . 9  |-  ran  h  e.  _V
130129, 52unex 4518 . . . . . . . 8  |-  ( ran  h  u.  { (/) } )  e.  _V
131 fex2 5401 . . . . . . . 8  |-  ( ( ( x  e.  om  |->  ( h `  x
) ) : om --> ( ran  h  u.  { (/)
} )  /\  om  e.  _V  /\  ( ran  h  u.  { (/) } )  e.  _V )  ->  ( x  e.  om  |->  ( h `  x
) )  e.  _V )
132126, 127, 130, 131mp3an 1277 . . . . . . 7  |-  ( x  e.  om  |->  ( h `
 x ) )  e.  _V
13395, 132eqeltri 2353 . . . . . 6  |-  G  e. 
_V
134 feq1 5375 . . . . . . 7  |-  ( g  =  G  ->  (
g : om --> A  <->  G : om
--> A ) )
135 fveq1 5524 . . . . . . . . 9  |-  ( g  =  G  ->  (
g `  suc  k )  =  ( G `  suc  k ) )
136 fveq1 5524 . . . . . . . . . 10  |-  ( g  =  G  ->  (
g `  k )  =  ( G `  k ) )
137136fveq2d 5529 . . . . . . . . 9  |-  ( g  =  G  ->  ( F `  ( g `  k ) )  =  ( F `  ( G `  k )
) )
138135, 137eleq12d 2351 . . . . . . . 8  |-  ( g  =  G  ->  (
( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) )
139138ralbidv 2563 . . . . . . 7  |-  ( g  =  G  ->  ( A. k  e.  om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <->  A. k  e.  om  ( G `  suc  k
)  e.  ( F `
 ( G `  k ) ) ) )
140134, 139anbi12d 691 . . . . . 6  |-  ( g  =  G  ->  (
( g : om --> A  /\  A. k  e. 
om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) )  <->  ( G : om
--> A  /\  A. k  e.  om  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) ) )
141133, 140spcev 2875 . . . . 5  |-  ( ( G : om --> A  /\  A. k  e.  om  ( G `  suc  k )  e.  ( F `  ( G `  k ) ) )  ->  E. g
( g : om --> A  /\  A. k  e. 
om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) )
14299, 121, 141syl2anc 642 . . . 4  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. g
( g : om --> A  /\  A. k  e. 
om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) )
143142ex 423 . . 3  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. g
( g : om --> A  /\  A. k  e. 
om  ( g `  suc  k )  e.  ( F `  ( g `
 k ) ) ) ) )
144143exlimiv 1666 . 2  |-  ( E. h A. k  e. 
om  ( h `  k ) R ( h `  suc  k
)  ->  ( F : A --> ( ~P A  \  { (/) } )  ->  E. g ( g : om --> A  /\  A. k  e.  om  (
g `  suc  k )  e.  ( F `  ( g `  k
) ) ) ) )
14579, 80, 144sylc 56 1  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. g ( g : om --> A  /\  A. k  e.  om  (
g `  suc  k )  e.  ( F `  ( g `  k
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684   {cab 2269    =/= wne 2446   A.wral 2543   {crab 2547   _Vcvv 2788    \ cdif 3149    u. cun 3150    C_ wss 3152   (/)c0 3455   ~Pcpw 3625   {csn 3640   U.cuni 3827   class class class wbr 4023   {copab 4076    e. cmpt 4077   suc csuc 4394   omcom 4656    X. cxp 4687   dom cdm 4689   ran crn 4690   -->wf 5251   ` cfv 5255
This theorem is referenced by:  axdc2  8075
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-dc 8072
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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263  df-1o 6479
  Copyright terms: Public domain W3C validator