# 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 $⊢ φ → A ∈ Fin$
marypha2.b $⊢ φ → F : A ⟶ Fin$
marypha2.c $⊢ φ ∧ d ⊆ A → d ≼ ⋃ F d$
Assertion marypha2 $⊢ φ → ∃ g g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$

### Proof

Step Hyp Ref Expression
1 marypha2.a $⊢ φ → A ∈ Fin$
2 marypha2.b $⊢ φ → F : A ⟶ Fin$
3 marypha2.c $⊢ φ ∧ d ⊆ A → d ≼ ⋃ F d$
4 2 1 unirnffid $⊢ φ → ⋃ ran ⁡ F ∈ Fin$
5 eqid $⊢ ⋃ x ∈ A x × F ⁡ x = ⋃ x ∈ A x × F ⁡ x$
6 5 marypha2lem1 $⊢ ⋃ x ∈ A x × F ⁡ x ⊆ A × ⋃ ran ⁡ F$
7 6 a1i $⊢ φ → ⋃ x ∈ A x × F ⁡ x ⊆ A × ⋃ ran ⁡ F$
8 2 ffnd $⊢ φ → F Fn A$
9 5 marypha2lem4 $⊢ F Fn A ∧ d ⊆ A → ⋃ x ∈ A x × F ⁡ x d = ⋃ F d$
10 8 9 sylan $⊢ φ ∧ d ⊆ A → ⋃ x ∈ A x × F ⁡ x d = ⋃ F d$
11 3 10 breqtrrd $⊢ φ ∧ d ⊆ A → d ≼ ⋃ x ∈ A x × F ⁡ x d$
12 1 4 7 11 marypha1 $⊢ φ → ∃ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x g : A ⟶ 1-1 ⋃ ran ⁡ F$
13 df-rex $⊢ ∃ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x g : A ⟶ 1-1 ⋃ ran ⁡ F ↔ ∃ g g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F$
14 ssv $⊢ ⋃ ran ⁡ F ⊆ V$
15 f1ss $⊢ g : A ⟶ 1-1 ⋃ ran ⁡ F ∧ ⋃ ran ⁡ F ⊆ V → g : A ⟶ 1-1 V$
16 14 15 mpan2 $⊢ g : A ⟶ 1-1 ⋃ ran ⁡ F → g : A ⟶ 1-1 V$
17 16 ad2antll $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g : A ⟶ 1-1 V$
18 elpwi $⊢ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x → g ⊆ ⋃ x ∈ A x × F ⁡ x$
19 18 ad2antrl $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g ⊆ ⋃ x ∈ A x × F ⁡ x$
20 f1fn $⊢ g : A ⟶ 1-1 ⋃ ran ⁡ F → g Fn A$
21 20 ad2antll $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g Fn A$
22 5 marypha2lem3 $⊢ F Fn A ∧ g Fn A → g ⊆ ⋃ x ∈ A x × F ⁡ x ↔ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
23 8 21 22 syl2an2r $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g ⊆ ⋃ x ∈ A x × F ⁡ x ↔ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
24 19 23 mpbid $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
25 17 24 jca $⊢ φ ∧ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
26 25 ex $⊢ φ → g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
27 26 eximdv $⊢ φ → ∃ g g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x ∧ g : A ⟶ 1-1 ⋃ ran ⁡ F → ∃ g g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
28 13 27 syl5bi $⊢ φ → ∃ g ∈ 𝒫 ⋃ x ∈ A x × F ⁡ x g : A ⟶ 1-1 ⋃ ran ⁡ F → ∃ g g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$
29 12 28 mpd $⊢ φ → ∃ g g : A ⟶ 1-1 V ∧ ∀ x ∈ A g ⁡ x ∈ F ⁡ x$