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

Theorem axdc2lem 8288
Description: Lemma for axdc2 8289. 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 8286 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 5831 . . . . . . . . 9  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  ( F `  x )  e.  ( ~P A  \  { (/) } ) )
2 eldifsni 3892 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  -> 
( F `  x
)  =/=  (/) )
3 n0 3601 . . . . . . . . . 10  |-  ( ( F `  x )  =/=  (/)  <->  E. y  y  e.  ( F `  x
) )
42, 3sylib 189 . . . . . . . . 9  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  ->  E. y  y  e.  ( F `  x ) )
51, 4syl 16 . . . . . . . 8  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  E. y 
y  e.  ( F `
 x ) )
65ralrimiva 2753 . . . . . . 7  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  A. x  e.  A  E. y 
y  e.  ( F `
 x ) )
7 rabid2 2849 . . . . . . 7  |-  ( A  =  { x  e.  A  |  E. y 
y  e.  ( F `
 x ) }  <->  A. x  e.  A  E. y  y  e.  ( F `  x ) )
86, 7sylibr 204 . . . . . 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 5034 . . . . . . 7  |-  dom  R  =  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x ) ) }
11 19.42v 1924 . . . . . . . . 9  |-  ( E. y ( x  e.  A  /\  y  e.  ( F `  x
) )  <->  ( x  e.  A  /\  E. y 
y  e.  ( F `
 x ) ) )
1211abbii 2520 . . . . . . . 8  |-  { x  |  E. y ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  |  (
x  e.  A  /\  E. y  y  e.  ( F `  x ) ) }
13 dmopab 5043 . . . . . . . 8  |-  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  |  E. y ( x  e.  A  /\  y  e.  ( F `  x
) ) }
14 df-rab 2679 . . . . . . . 8  |-  { x  e.  A  |  E. y  y  e.  ( F `  x ) }  =  { x  |  ( x  e.  A  /\  E. y 
y  e.  ( F `
 x ) ) }
1512, 13, 143eqtr4i 2438 . . . . . . 7  |-  dom  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { x  e.  A  |  E. y  y  e.  ( F `  x
) }
1610, 15eqtri 2428 . . . . . 6  |-  dom  R  =  { x  e.  A  |  E. y  y  e.  ( F `  x
) }
178, 16syl6reqr 2459 . . . . 5  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  dom  R  =  A )
1817neeq1d 2584 . . . 4  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( dom  R  =/=  (/)  <->  A  =/=  (/) ) )
1918biimparc 474 . . 3  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  dom  R  =/=  (/) )
20 eldifi 3433 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ( ~P A  \  { (/) } )  -> 
( F `  x
)  e.  ~P A
)
21 elelpwi 3773 . . . . . . . . . . 11  |-  ( ( y  e.  ( F `
 x )  /\  ( F `  x )  e.  ~P A )  ->  y  e.  A
)
2221expcom 425 . . . . . . . . . 10  |-  ( ( F `  x )  e.  ~P A  -> 
( y  e.  ( F `  x )  ->  y  e.  A
) )
231, 20, 223syl 19 . . . . . . . . 9  |-  ( ( F : A --> ( ~P A  \  { (/) } )  /\  x  e.  A )  ->  (
y  e.  ( F `
 x )  -> 
y  e.  A ) )
2423expimpd 587 . . . . . . . 8  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( (
x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
2524exlimdv 1643 . . . . . . 7  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( E. x ( x  e.  A  /\  y  e.  ( F `  x
) )  ->  y  e.  A ) )
2625alrimiv 1638 . . . . . 6  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  A. y
( E. x ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
279rneqi 5059 . . . . . . . . 9  |-  ran  R  =  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x ) ) }
28 rnopab 5078 . . . . . . . . 9  |-  ran  { <. x ,  y >.  |  ( x  e.  A  /\  y  e.  ( F `  x
) ) }  =  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }
2927, 28eqtri 2428 . . . . . . . 8  |-  ran  R  =  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }
3029sseq1i 3336 . . . . . . 7  |-  ( ran 
R  C_  A  <->  { y  |  E. x ( x  e.  A  /\  y  e.  ( F `  x
) ) }  C_  A )
31 abss 3376 . . . . . . 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 241 . . . . . 6  |-  ( ran 
R  C_  A  <->  A. y
( E. x ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
y  e.  A ) )
3326, 32sylibr 204 . . . . 5  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  R  C_  A )
3433, 17sseqtr4d 3349 . . . 4  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  R  C_  dom  R )
3534adantl 453 . . 3  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  R  C_  dom  R )
36 fvrn0 5716 . . . . . . . . . 10  |-  ( F `
 x )  e.  ( ran  F  u.  {
(/) } )
37 elssuni 4007 . . . . . . . . . 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 3308 . . . . . . . 8  |-  ( y  e.  ( F `  x )  ->  y  e.  U. ( ran  F  u.  { (/) } ) )
4039anim2i 553 . . . . . . 7  |-  ( ( x  e.  A  /\  y  e.  ( F `  x ) )  -> 
( x  e.  A  /\  y  e.  U. ( ran  F  u.  { (/) } ) ) )
4140ssopab2i 4446 . . . . . 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 4847 . . . . . 6  |-  ( A  X.  U. ( ran 
F  u.  { (/) } ) )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  e. 
U. ( ran  F  u.  { (/) } ) ) }
4341, 9, 423sstr4i 3351 . . . . 5  |-  R  C_  ( A  X.  U. ( ran  F  u.  { (/) } ) )
44 axdc2lem.1 . . . . . 6  |-  A  e. 
_V
45 frn 5560 . . . . . . . . . 10  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ran  F  C_  ( ~P A  \  { (/)
} ) )
4645adantl 453 . . . . . . . . 9  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  F  C_  ( ~P A  \  { (/) } ) )
4744pwex 4346 . . . . . . . . . . 11  |-  ~P A  e.  _V
48 difexg 4315 . . . . . . . . . . 11  |-  ( ~P A  e.  _V  ->  ( ~P A  \  { (/)
} )  e.  _V )
4947, 48ax-mp 8 . . . . . . . . . 10  |-  ( ~P A  \  { (/) } )  e.  _V
5049ssex 4311 . . . . . . . . 9  |-  ( ran 
F  C_  ( ~P A  \  { (/) } )  ->  ran  F  e.  _V )
5146, 50syl 16 . . . . . . . 8  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ran  F  e.  _V )
52 p0ex 4350 . . . . . . . 8  |-  { (/) }  e.  _V
53 unexg 4673 . . . . . . . 8  |-  ( ( ran  F  e.  _V  /\ 
{ (/) }  e.  _V )  ->  ( ran  F  u.  { (/) } )  e. 
_V )
5451, 52, 53sylancl 644 . . . . . . 7  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ( ran  F  u.  { (/) } )  e. 
_V )
55 uniexg 4669 . . . . . . 7  |-  ( ( ran  F  u.  { (/)
} )  e.  _V  ->  U. ( ran  F  u.  { (/) } )  e. 
_V )
5654, 55syl 16 . . . . . 6  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  U. ( ran  F  u.  { (/) } )  e. 
_V )
57 xpexg 4952 . . . . . 6  |-  ( ( A  e.  _V  /\  U. ( ran  F  u.  {
(/) } )  e.  _V )  ->  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )
5844, 56, 57sylancr 645 . . . . 5  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )
59 ssexg 4313 . . . . 5  |-  ( ( R  C_  ( A  X.  U. ( ran  F  u.  { (/) } ) )  /\  ( A  X.  U. ( ran  F  u.  {
(/) } ) )  e. 
_V )  ->  R  e.  _V )
6043, 58, 59sylancr 645 . . . 4  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  R  e.  _V )
61 n0 3601 . . . . . . . . 9  |-  ( dom  r  =/=  (/)  <->  E. x  x  e.  dom  r )
62 vex 2923 . . . . . . . . . . 11  |-  x  e. 
_V
6362eldm 5030 . . . . . . . . . 10  |-  ( x  e.  dom  r  <->  E. y  x r y )
6463exbii 1589 . . . . . . . . 9  |-  ( E. x  x  e.  dom  r 
<->  E. x E. y  x r y )
6561, 64bitr2i 242 . . . . . . . 8  |-  ( E. x E. y  x r y  <->  dom  r  =/=  (/) )
66 dmeq 5033 . . . . . . . . 9  |-  ( r  =  R  ->  dom  r  =  dom  R )
6766neeq1d 2584 . . . . . . . 8  |-  ( r  =  R  ->  ( dom  r  =/=  (/)  <->  dom  R  =/=  (/) ) )
6865, 67syl5bb 249 . . . . . . 7  |-  ( r  =  R  ->  ( E. x E. y  x r y  <->  dom  R  =/=  (/) ) )
69 rneq 5058 . . . . . . . 8  |-  ( r  =  R  ->  ran  r  =  ran  R )
7069, 66sseq12d 3341 . . . . . . 7  |-  ( r  =  R  ->  ( ran  r  C_  dom  r  <->  ran 
R  C_  dom  R ) )
7168, 70anbi12d 692 . . . . . 6  |-  ( r  =  R  ->  (
( E. x E. y  x r y  /\  ran  r  C_  dom  r
)  <->  ( dom  R  =/=  (/)  /\  ran  R  C_ 
dom  R ) ) )
72 breq 4178 . . . . . . . 8  |-  ( r  =  R  ->  (
( h `  k
) r ( h `
 suc  k )  <->  ( h `  k ) R ( h `  suc  k ) ) )
7372ralbidv 2690 . . . . . . 7  |-  ( r  =  R  ->  ( A. k  e.  om  ( h `  k
) r ( h `
 suc  k )  <->  A. k  e.  om  (
h `  k ) R ( h `  suc  k ) ) )
7473exbidv 1633 . . . . . 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 312 . . . . 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 8286 . . . . 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 2975 . . . 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 16 . . 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 661 . 2  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  E. h A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )
80 simpr 448 . 2  |-  ( ( A  =/=  (/)  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  F : A --> ( ~P A  \  { (/)
} ) )
81 fveq2 5691 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
h `  k )  =  ( h `  x ) )
82 suceq 4610 . . . . . . . . . . . . . . . 16  |-  ( k  =  x  ->  suc  k  =  suc  x )
8382fveq2d 5695 . . . . . . . . . . . . . . 15  |-  ( k  =  x  ->  (
h `  suc  k )  =  ( h `  suc  x ) )
8481, 83breq12d 4189 . . . . . . . . . . . . . 14  |-  ( k  =  x  ->  (
( h `  k
) R ( h `
 suc  k )  <->  ( h `  x ) R ( h `  suc  x ) ) )
8584rspccv 3013 . . . . . . . . . . . . 13  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  (
x  e.  om  ->  ( h `  x ) R ( h `  suc  x ) ) )
86 fvex 5705 . . . . . . . . . . . . . 14  |-  ( h `
 x )  e. 
_V
87 fvex 5705 . . . . . . . . . . . . . 14  |-  ( h `
 suc  x )  e.  _V
8886, 87breldm 5037 . . . . . . . . . . . . 13  |-  ( ( h `  x ) R ( h `  suc  x )  ->  (
h `  x )  e.  dom  R )
8985, 88syl6 31 . . . . . . . . . . . 12  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  (
x  e.  om  ->  ( h `  x )  e.  dom  R ) )
9089imp 419 . . . . . . . . . . 11  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  x  e.  om )  ->  ( h `  x )  e.  dom  R )
9190adantll 695 . . . . . . . . . 10  |-  ( ( ( dom  R  =  A  /\  A. k  e.  om  ( h `  k ) R ( h `  suc  k
) )  /\  x  e.  om )  ->  (
h `  x )  e.  dom  R )
92 eleq2 2469 . . . . . . . . . . 11  |-  ( dom 
R  =  A  -> 
( ( h `  x )  e.  dom  R  <-> 
( h `  x
)  e.  A ) )
9392ad2antrr 707 . . . . . . . . . 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 202 . . . . . . . . 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 5856 . . . . . . . 8  |-  ( ( dom  R  =  A  /\  A. k  e. 
om  ( h `  k ) R ( h `  suc  k
) )  ->  G : om --> A )
9796ex 424 . . . . . . 7  |-  ( dom 
R  =  A  -> 
( A. k  e. 
om  ( h `  k ) R ( h `  suc  k
)  ->  G : om
--> A ) )
9817, 97syl 16 . . . . . 6  |-  ( F : A --> ( ~P A  \  { (/) } )  ->  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  G : om --> A ) )
9998impcom 420 . . . . 5  |-  ( ( A. k  e.  om  ( h `  k
) R ( h `
 suc  k )  /\  F : A --> ( ~P A  \  { (/) } ) )  ->  G : om --> A )
100 fveq2 5691 . . . . . . . . . 10  |-  ( x  =  k  ->  (
h `  x )  =  ( h `  k ) )
101 fvex 5705 . . . . . . . . . 10  |-  ( h `
 k )  e. 
_V
102100, 95, 101fvmpt 5769 . . . . . . . . 9  |-  ( k  e.  om  ->  ( G `  k )  =  ( h `  k ) )
103 peano2 4828 . . . . . . . . . 10  |-  ( k  e.  om  ->  suc  k  e.  om )
104 fvex 5705 . . . . . . . . . 10  |-  ( h `
 suc  k )  e.  _V
105 fveq2 5691 . . . . . . . . . . 11  |-  ( x  =  suc  k  -> 
( h `  x
)  =  ( h `
 suc  k )
)
106105, 95fvmptg 5767 . . . . . . . . . 10  |-  ( ( suc  k  e.  om  /\  ( h `  suc  k )  e.  _V )  ->  ( G `  suc  k )  =  ( h `  suc  k
) )
107103, 104, 106sylancl 644 . . . . . . . . 9  |-  ( k  e.  om  ->  ( G `  suc  k )  =  ( h `  suc  k ) )
108102, 107breq12d 4189 . . . . . . . 8  |-  ( k  e.  om  ->  (
( G `  k
) R ( G `
 suc  k )  <->  ( h `  k ) R ( h `  suc  k ) ) )
109 fvex 5705 . . . . . . . . . 10  |-  ( G `
 k )  e. 
_V
110 fvex 5705 . . . . . . . . . 10  |-  ( G `
 suc  k )  e.  _V
111 eleq1 2468 . . . . . . . . . . 11  |-  ( x  =  ( G `  k )  ->  (
x  e.  A  <->  ( G `  k )  e.  A
) )
112 fveq2 5691 . . . . . . . . . . . 12  |-  ( x  =  ( G `  k )  ->  ( F `  x )  =  ( F `  ( G `  k ) ) )
113112eleq2d 2475 . . . . . . . . . . 11  |-  ( x  =  ( G `  k )  ->  (
y  e.  ( F `
 x )  <->  y  e.  ( F `  ( G `
 k ) ) ) )
114111, 113anbi12d 692 . . . . . . . . . 10  |-  ( x  =  ( G `  k )  ->  (
( x  e.  A  /\  y  e.  ( F `  x )
)  <->  ( ( G `
 k )  e.  A  /\  y  e.  ( F `  ( G `  k )
) ) ) )
115 eleq1 2468 . . . . . . . . . . 11  |-  ( y  =  ( G `  suc  k )  ->  (
y  e.  ( F `
 ( G `  k ) )  <->  ( G `  suc  k )  e.  ( F `  ( G `  k )
) ) )
116115anbi2d 685 . . . . . . . . . 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 4441 . . . . . . . . 9  |-  ( ( G `  k ) R ( G `  suc  k )  <->  ( ( G `  k )  e.  A  /\  ( G `  suc  k )  e.  ( F `  ( G `  k ) ) ) )
118117simprbi 451 . . . . . . . 8  |-  ( ( G `  k ) R ( G `  suc  k )  ->  ( G `  suc  k )  e.  ( F `  ( G `  k ) ) )
119108, 118syl6bir 221 . . . . . . 7  |-  ( k  e.  om  ->  (
( h `  k
) R ( h `
 suc  k )  ->  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) )
120119ralimia 2743 . . . . . 6  |-  ( A. k  e.  om  (
h `  k ) R ( h `  suc  k )  ->  A. k  e.  om  ( G `  suc  k )  e.  ( F `  ( G `
 k ) ) )
121120adantr 452 . . . . 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 5716 . . . . . . . . . 10  |-  ( h `
 x )  e.  ( ran  h  u. 
{ (/) } )
123122rgenw 2737 . . . . . . . . 9  |-  A. x  e.  om  ( h `  x )  e.  ( ran  h  u.  { (/)
} )
124 eqid 2408 . . . . . . . . . 10  |-  ( x  e.  om  |->  ( h `
 x ) )  =  ( x  e. 
om  |->  ( h `  x ) )
125124fmpt 5853 . . . . . . . . 9  |-  ( A. x  e.  om  (
h `  x )  e.  ( ran  h  u. 
{ (/) } )  <->  ( x  e.  om  |->  ( h `  x ) ) : om --> ( ran  h  u.  { (/) } ) )
126123, 125mpbi 200 . . . . . . . 8  |-  ( x  e.  om  |->  ( h `
 x ) ) : om --> ( ran  h  u.  { (/) } )
127 dcomex 8287 . . . . . . . 8  |-  om  e.  _V
128 vex 2923 . . . . . . . . . 10  |-  h  e. 
_V
129128rnex 5096 . . . . . . . . 9  |-  ran  h  e.  _V
130129, 52unex 4670 . . . . . . . 8  |-  ( ran  h  u.  { (/) } )  e.  _V
131 fex2 5566 . . . . . . . 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 1279 . . . . . . 7  |-  ( x  e.  om  |->  ( h `
 x ) )  e.  _V
13395, 132eqeltri 2478 . . . . . 6  |-  G  e. 
_V
134 feq1 5539 . . . . . . 7  |-  ( g  =  G  ->  (
g : om --> A  <->  G : om
--> A ) )
135 fveq1 5690 . . . . . . . . 9  |-  ( g  =  G  ->  (
g `  suc  k )  =  ( G `  suc  k ) )
136 fveq1 5690 . . . . . . . . . 10  |-  ( g  =  G  ->  (
g `  k )  =  ( G `  k ) )
137136fveq2d 5695 . . . . . . . . 9  |-  ( g  =  G  ->  ( F `  ( g `  k ) )  =  ( F `  ( G `  k )
) )
138135, 137eleq12d 2476 . . . . . . . 8  |-  ( g  =  G  ->  (
( g `  suc  k )  e.  ( F `  ( g `
 k ) )  <-> 
( G `  suc  k )  e.  ( F `  ( G `
 k ) ) ) )
139138ralbidv 2690 . . . . . . 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 692 . . . . . 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 3007 . . . . 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 643 . . . 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 424 . . 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 1641 . 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 58 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 177    /\ wa 359   A.wal 1546   E.wex 1547    = wceq 1649    e. wcel 1721   {cab 2394    =/= wne 2571   A.wral 2670   {crab 2674   _Vcvv 2920    \ cdif 3281    u. cun 3282    C_ wss 3284   (/)c0 3592   ~Pcpw 3763   {csn 3778   U.cuni 3979   class class class wbr 4176   {copab 4229    e. cmpt 4230   suc csuc 4547   omcom 4808    X. cxp 4839   dom cdm 4841   ran crn 4842   -->wf 5413   ` cfv 5417
This theorem is referenced by:  axdc2  8289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-dc 8286
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-fv 5425  df-1o 6687
  Copyright terms: Public domain W3C validator