# 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 ( 𝜑𝐴 ∈ Fin )
marypha2.b ( 𝜑𝐹 : 𝐴 ⟶ Fin )
marypha2.c ( ( 𝜑𝑑𝐴 ) → 𝑑 ( 𝐹𝑑 ) )
Assertion marypha2 ( 𝜑 → ∃ 𝑔 ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) )

### Proof

Step Hyp Ref Expression
1 marypha2.a ( 𝜑𝐴 ∈ Fin )
2 marypha2.b ( 𝜑𝐹 : 𝐴 ⟶ Fin )
3 marypha2.c ( ( 𝜑𝑑𝐴 ) → 𝑑 ( 𝐹𝑑 ) )
4 2 1 unirnffid ( 𝜑 ran 𝐹 ∈ Fin )
5 eqid 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) = 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) )
6 5 marypha2lem1 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ⊆ ( 𝐴 × ran 𝐹 )
7 6 a1i ( 𝜑 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ⊆ ( 𝐴 × ran 𝐹 ) )
8 2 ffnd ( 𝜑𝐹 Fn 𝐴 )
9 5 marypha2lem4 ( ( 𝐹 Fn 𝐴𝑑𝐴 ) → ( 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) “ 𝑑 ) = ( 𝐹𝑑 ) )
10 8 9 sylan ( ( 𝜑𝑑𝐴 ) → ( 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) “ 𝑑 ) = ( 𝐹𝑑 ) )
11 3 10 breqtrrd ( ( 𝜑𝑑𝐴 ) → 𝑑 ≼ ( 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) “ 𝑑 ) )
12 1 4 7 11 marypha1 ( 𝜑 → ∃ 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) 𝑔 : 𝐴1-1 ran 𝐹 )
13 df-rex ( ∃ 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) 𝑔 : 𝐴1-1 ran 𝐹 ↔ ∃ 𝑔 ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) )
14 ssv ran 𝐹 ⊆ V
15 f1ss ( ( 𝑔 : 𝐴1-1 ran 𝐹 ran 𝐹 ⊆ V ) → 𝑔 : 𝐴1-1→ V )
16 14 15 mpan2 ( 𝑔 : 𝐴1-1 ran 𝐹𝑔 : 𝐴1-1→ V )
17 16 ad2antll ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → 𝑔 : 𝐴1-1→ V )
18 elpwi ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) → 𝑔 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) )
19 18 ad2antrl ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → 𝑔 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) )
20 f1fn ( 𝑔 : 𝐴1-1 ran 𝐹𝑔 Fn 𝐴 )
21 20 ad2antll ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → 𝑔 Fn 𝐴 )
22 5 marypha2lem3 ( ( 𝐹 Fn 𝐴𝑔 Fn 𝐴 ) → ( 𝑔 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ↔ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) )
23 8 21 22 syl2an2r ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → ( 𝑔 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ↔ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) )
24 19 23 mpbid ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) )
25 17 24 jca ( ( 𝜑 ∧ ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) ) → ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) )
26 25 ex ( 𝜑 → ( ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) → ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) ) )
27 26 eximdv ( 𝜑 → ( ∃ 𝑔 ( 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) ∧ 𝑔 : 𝐴1-1 ran 𝐹 ) → ∃ 𝑔 ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) ) )
28 13 27 syl5bi ( 𝜑 → ( ∃ 𝑔 ∈ 𝒫 𝑥𝐴 ( { 𝑥 } × ( 𝐹𝑥 ) ) 𝑔 : 𝐴1-1 ran 𝐹 → ∃ 𝑔 ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) ) )
29 12 28 mpd ( 𝜑 → ∃ 𝑔 ( 𝑔 : 𝐴1-1→ V ∧ ∀ 𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝐹𝑥 ) ) )