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

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