Metamath Proof Explorer

Theorem unirnfdomd

Description: The union of the range of a function from an infinite set into the class of finite sets is dominated by its domain. Deduction form. (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses unirnfdomd.1 ⊢ φ → F : T ⟶ Fin
unirnfdomd.2 ⊢ φ → ¬ T ∈ Fin
unirnfdomd.3 ⊢ φ → T ∈ V
Assertion unirnfdomd ⊢ φ → ⋃ ran ⁡ F ≼ T

Proof

Step Hyp Ref Expression
1 unirnfdomd.1 ⊢ φ → F : T ⟶ Fin
2 unirnfdomd.2 ⊢ φ → ¬ T ∈ Fin
3 unirnfdomd.3 ⊢ φ → T ∈ V
4 1 ffnd ⊢ φ → F Fn T
5 fnex ⊢ F Fn T ∧ T ∈ V → F ∈ V
6 4 3 5 syl2anc ⊢ φ → F ∈ V
7 rnexg ⊢ F ∈ V → ran ⁡ F ∈ V
8 6 7 syl ⊢ φ → ran ⁡ F ∈ V
9 frn ⊢ F : T ⟶ Fin → ran ⁡ F ⊆ Fin
10 dfss3 ⊢ ran ⁡ F ⊆ Fin ↔ ∀ x ∈ ran ⁡ F x ∈ Fin
11 9 10 sylib ⊢ F : T ⟶ Fin → ∀ x ∈ ran ⁡ F x ∈ Fin
12 fict ⊢ x ∈ Fin → x ≼ ω
13 12 ralimi ⊢ ∀ x ∈ ran ⁡ F x ∈ Fin → ∀ x ∈ ran ⁡ F x ≼ ω
14 1 11 13 3syl ⊢ φ → ∀ x ∈ ran ⁡ F x ≼ ω
15 unidom ⊢ ran ⁡ F ∈ V ∧ ∀ x ∈ ran ⁡ F x ≼ ω → ⋃ ran ⁡ F ≼ ran ⁡ F × ω
16 8 14 15 syl2anc ⊢ φ → ⋃ ran ⁡ F ≼ ran ⁡ F × ω
17 fnrndomg ⊢ T ∈ V → F Fn T → ran ⁡ F ≼ T
18 3 4 17 sylc ⊢ φ → ran ⁡ F ≼ T
19 omex ⊢ ω ∈ V
20 19 xpdom1 ⊢ ran ⁡ F ≼ T → ran ⁡ F × ω ≼ T × ω
21 18 20 syl ⊢ φ → ran ⁡ F × ω ≼ T × ω
22 domtr ⊢ ⋃ ran ⁡ F ≼ ran ⁡ F × ω ∧ ran ⁡ F × ω ≼ T × ω → ⋃ ran ⁡ F ≼ T × ω
23 16 21 22 syl2anc ⊢ φ → ⋃ ran ⁡ F ≼ T × ω
24 infinf ⊢ T ∈ V → ¬ T ∈ Fin ↔ ω ≼ T
25 3 24 syl ⊢ φ → ¬ T ∈ Fin ↔ ω ≼ T
26 2 25 mpbid ⊢ φ → ω ≼ T
27 xpdom2g ⊢ T ∈ V ∧ ω ≼ T → T × ω ≼ T × T
28 3 26 27 syl2anc ⊢ φ → T × ω ≼ T × T
29 domtr ⊢ ⋃ ran ⁡ F ≼ T × ω ∧ T × ω ≼ T × T → ⋃ ran ⁡ F ≼ T × T
30 23 28 29 syl2anc ⊢ φ → ⋃ ran ⁡ F ≼ T × T
31 infxpidm ⊢ ω ≼ T → T × T ≈ T
32 26 31 syl ⊢ φ → T × T ≈ T
33 domentr ⊢ ⋃ ran ⁡ F ≼ T × T ∧ T × T ≈ T → ⋃ ran ⁡ F ≼ T
34 30 32 33 syl2anc ⊢ φ → ⋃ ran ⁡ F ≼ T