Theorem hfrel

Description: A relation is a hereditarily finite set iff its domain and range are. (Contributed by Eric Schmidt, 26-Sep-2026)

	Ref	Expression
Assertion	hfrel	⊢ ( Rel 𝑅 → ( 𝑅 ∈ HF ↔ ( dom 𝑅 ∈ HF ∧ ran 𝑅 ∈ HF ) ) )

Proof

Step	Hyp	Ref	Expression
1		hfdm	⊢ ( 𝑅 ∈ HF → dom 𝑅 ∈ HF )
2		hfrn	⊢ ( 𝑅 ∈ HF → ran 𝑅 ∈ HF )
3	1 2	jca	⊢ ( 𝑅 ∈ HF → ( dom 𝑅 ∈ HF ∧ ran 𝑅 ∈ HF ) )
4		hfxp	⊢ ( ( dom 𝑅 ∈ HF ∧ ran 𝑅 ∈ HF ) → ( dom 𝑅 × ran 𝑅 ) ∈ HF )
5		relssdmrn	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
6		hfsshf	⊢ ( ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ∧ ( dom 𝑅 × ran 𝑅 ) ∈ HF ) → 𝑅 ∈ HF )
7	5 6	sylan	⊢ ( ( Rel 𝑅 ∧ ( dom 𝑅 × ran 𝑅 ) ∈ HF ) → 𝑅 ∈ HF )
8	7	ex	⊢ ( Rel 𝑅 → ( ( dom 𝑅 × ran 𝑅 ) ∈ HF → 𝑅 ∈ HF ) )
9	4 8	syl5	⊢ ( Rel 𝑅 → ( ( dom 𝑅 ∈ HF ∧ ran 𝑅 ∈ HF ) → 𝑅 ∈ HF ) )
10	3 9	impbid2	⊢ ( Rel 𝑅 → ( 𝑅 ∈ HF ↔ ( dom 𝑅 ∈ HF ∧ ran 𝑅 ∈ HF ) ) )