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	⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ Fin )
	unirnfdomd.2	⊢ ( 𝜑 → ¬ 𝑇 ∈ Fin )
	unirnfdomd.3	⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion	unirnfdomd	⊢ ( 𝜑 → ∪ ran 𝐹 ≼ 𝑇 )

Proof

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