Theorem unfir

Description: If a union is finite, the operands are finite. Converse of unfi . (Contributed by FL, 3-Aug-2009)

	Ref	Expression
Assertion	unfir	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2		ssfi	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) ) → 𝐴 ∈ Fin )
3	1 2	mpan2	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → 𝐴 ∈ Fin )
4		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
5		ssfi	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) ) → 𝐵 ∈ Fin )
6	4 5	mpan2	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → 𝐵 ∈ Fin )
7	3 6	jca	⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) )