This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem unirnffid

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

Ref Expression
Hypotheses unirnffid.1 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ Fin )
unirnffid.2 ⊢ ( 𝜑 → 𝑇 ∈ Fin )
Assertion unirnffid ( 𝜑 → ∪ ran 𝐹 ∈ Fin )

Proof

Step Hyp Ref Expression
1 unirnffid.1 ⊢ ( 𝜑 → 𝐹 : 𝑇 ⟶ Fin )
2 unirnffid.2 ⊢ ( 𝜑 → 𝑇 ∈ Fin )
3 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑇 )
4 fnfi ⊢ ( ( 𝐹 Fn 𝑇 ∧ 𝑇 ∈ Fin ) → 𝐹 ∈ Fin )
5 3 2 4 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ Fin )
6 rnfi ⊢ ( 𝐹 ∈ Fin → ran 𝐹 ∈ Fin )
7 5 6 syl ⊢ ( 𝜑 → ran 𝐹 ∈ Fin )
8 1 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ Fin )
9 unifi ⊢ ( ( ran 𝐹 ∈ Fin ∧ ran 𝐹 ⊆ Fin ) → ∪ ran 𝐹 ∈ Fin )
10 7 8 9 syl2anc ⊢ ( 𝜑 → ∪ ran 𝐹 ∈ Fin )