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 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) )