# 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 )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`
` |-  ( ( 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 ) ) )`