Theorem relfi

Description: A relation (set) is finite if and only if both its domain and range are finite. (Contributed by Thierry Arnoux, 27-Aug-2017)

	Ref	Expression
Assertion	relfi	⊢ ( Rel 𝐴 → ( 𝐴 ∈ Fin ↔ ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmfi	⊢ ( 𝐴 ∈ Fin → dom 𝐴 ∈ Fin )
2		rnfi	⊢ ( 𝐴 ∈ Fin → ran 𝐴 ∈ Fin )
3	1 2	jca	⊢ ( 𝐴 ∈ Fin → ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) )
4		xpfi	⊢ ( ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) → ( dom 𝐴 × ran 𝐴 ) ∈ Fin )
5		relssdmrn	⊢ ( Rel 𝐴 → 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) )
6		ssfi	⊢ ( ( ( dom 𝐴 × ran 𝐴 ) ∈ Fin ∧ 𝐴 ⊆ ( dom 𝐴 × ran 𝐴 ) ) → 𝐴 ∈ Fin )
7	4 5 6	syl2anr	⊢ ( ( Rel 𝐴 ∧ ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) ) → 𝐴 ∈ Fin )
8	7	ex	⊢ ( Rel 𝐴 → ( ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) → 𝐴 ∈ Fin ) )
9	3 8	impbid2	⊢ ( Rel 𝐴 → ( 𝐴 ∈ Fin ↔ ( dom 𝐴 ∈ Fin ∧ ran 𝐴 ∈ Fin ) ) )