Metamath Proof Explorer


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 ) ) )