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 R -> ( R e. HF <-> ( dom R e. HF /\ ran R e. HF ) ) )

Proof

Step	Hyp	Ref	Expression
1		hfdm	|- ( R e. HF -> dom R e. HF )
2		hfrn	|- ( R e. HF -> ran R e. HF )
3	1 2	jca	|- ( R e. HF -> ( dom R e. HF /\ ran R e. HF ) )
4		hfxp	|- ( ( dom R e. HF /\ ran R e. HF ) -> ( dom R X. ran R ) e. HF )
5		relssdmrn	|- ( Rel R -> R C_ ( dom R X. ran R ) )
6		hfsshf	|- ( ( R C_ ( dom R X. ran R ) /\ ( dom R X. ran R ) e. HF ) -> R e. HF )
7	5 6	sylan	|- ( ( Rel R /\ ( dom R X. ran R ) e. HF ) -> R e. HF )
8	7	ex	|- ( Rel R -> ( ( dom R X. ran R ) e. HF -> R e. HF ) )
9	4 8	syl5	|- ( Rel R -> ( ( dom R e. HF /\ ran R e. HF ) -> R e. HF ) )
10	3 9	impbid2	|- ( Rel R -> ( R e. HF <-> ( dom R e. HF /\ ran R e. HF ) ) )