Metamath Proof Explorer

Theorem marypha2

Description: Version of marypha1 using a functional family of sets instead of a relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

Ref Expression
Hypotheses marypha2.a 
|- ( ph -> A e. Fin )
marypha2.b 
|- ( ph -> F : A --> Fin )
marypha2.c 
|- ( ( ph /\ d C_ A ) -> d ~<_ U. ( F " d ) )
Assertion marypha2 
|- ( ph -> E. g ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 marypha2.a 
 |-  ( ph -> A e. Fin )
2 marypha2.b 
 |-  ( ph -> F : A --> Fin )
3 marypha2.c 
 |-  ( ( ph /\ d C_ A ) -> d ~<_ U. ( F " d ) )
4 2 1 unirnffid 
 |-  ( ph -> U. ran F e. Fin )
5 eqid 
 |-  U_ x e. A ( { x } X. ( F ` x ) ) = U_ x e. A ( { x } X. ( F ` x ) )
6 5 marypha2lem1 
 |-  U_ x e. A ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F )
7 6 a1i 
 |-  ( ph -> U_ x e. A ( { x } X. ( F ` x ) ) C_ ( A X. U. ran F ) )
8 2 ffnd 
 |-  ( ph -> F Fn A )
9 5 marypha2lem4 
 |-  ( ( F Fn A /\ d C_ A ) -> ( U_ x e. A ( { x } X. ( F ` x ) ) " d ) = U. ( F " d ) )
10 8 9 sylan 
 |-  ( ( ph /\ d C_ A ) -> ( U_ x e. A ( { x } X. ( F ` x ) ) " d ) = U. ( F " d ) )
11 3 10 breqtrrd 
 |-  ( ( ph /\ d C_ A ) -> d ~<_ ( U_ x e. A ( { x } X. ( F ` x ) ) " d ) )
12 1 4 7 11 marypha1 
 |-  ( ph -> E. g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) g : A -1-1-> U. ran F )
13 df-rex 
 |-  ( E. g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) g : A -1-1-> U. ran F <-> E. g ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) )
14 ssv 
 |-  U. ran F C_ _V
15 f1ss 
 |-  ( ( g : A -1-1-> U. ran F /\ U. ran F C_ _V ) -> g : A -1-1-> _V )
16 14 15 mpan2 
 |-  ( g : A -1-1-> U. ran F -> g : A -1-1-> _V )
17 16 ad2antll 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> g : A -1-1-> _V )
18 elpwi 
 |-  ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) -> g C_ U_ x e. A ( { x } X. ( F ` x ) ) )
19 18 ad2antrl 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> g C_ U_ x e. A ( { x } X. ( F ` x ) ) )
20 f1fn 
 |-  ( g : A -1-1-> U. ran F -> g Fn A )
21 20 ad2antll 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> g Fn A )
22 5 marypha2lem3 
 |-  ( ( F Fn A /\ g Fn A ) -> ( g C_ U_ x e. A ( { x } X. ( F ` x ) ) <-> A. x e. A ( g ` x ) e. ( F ` x ) ) )
23 8 21 22 syl2an2r 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> ( g C_ U_ x e. A ( { x } X. ( F ` x ) ) <-> A. x e. A ( g ` x ) e. ( F ` x ) ) )
24 19 23 mpbid 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> A. x e. A ( g ` x ) e. ( F ` x ) )
25 17 24 jca 
 |-  ( ( ph /\ ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) ) -> ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) )
26 25 ex 
 |-  ( ph -> ( ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) -> ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) ) )
27 26 eximdv 
 |-  ( ph -> ( E. g ( g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) /\ g : A -1-1-> U. ran F ) -> E. g ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) ) )
28 13 27 syl5bi 
 |-  ( ph -> ( E. g e. ~P U_ x e. A ( { x } X. ( F ` x ) ) g : A -1-1-> U. ran F -> E. g ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) ) )
29 12 28 mpd 
 |-  ( ph -> E. g ( g : A -1-1-> _V /\ A. x e. A ( g ` x ) e. ( F ` x ) ) )