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	Could not format assertion : No typesetting found for |- ( Rel R -> ( R e. HF <-> ( dom R e. HF /\ ran R e. HF ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hfdm	Could not format ( R e. HF -> dom R e. HF ) : No typesetting found for |- ( R e. HF -> dom R e. HF ) with typecode |-
2		hfrn	Could not format ( R e. HF -> ran R e. HF ) : No typesetting found for |- ( R e. HF -> ran R e. HF ) with typecode |-
3	1 2	jca	Could not format ( R e. HF -> ( dom R e. HF /\ ran R e. HF ) ) : No typesetting found for |- ( R e. HF -> ( dom R e. HF /\ ran R e. HF ) ) with typecode |-
4		hfxp	Could not format ( ( dom R e. HF /\ ran R e. HF ) -> ( dom R X. ran R ) e. HF ) : No typesetting found for |- ( ( dom R e. HF /\ ran R e. HF ) -> ( dom R X. ran R ) e. HF ) with typecode |-
5		relssdmrn	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
6		hfsshf	Could not format ( ( R C_ ( dom R X. ran R ) /\ ( dom R X. ran R ) e. HF ) -> R e. HF ) : No typesetting found for |- ( ( R C_ ( dom R X. ran R ) /\ ( dom R X. ran R ) e. HF ) -> R e. HF ) with typecode |-
7	5 6	sylan	Could not format ( ( Rel R /\ ( dom R X. ran R ) e. HF ) -> R e. HF ) : No typesetting found for |- ( ( Rel R /\ ( dom R X. ran R ) e. HF ) -> R e. HF ) with typecode |-
8	7	ex	Could not format ( Rel R -> ( ( dom R X. ran R ) e. HF -> R e. HF ) ) : No typesetting found for |- ( Rel R -> ( ( dom R X. ran R ) e. HF -> R e. HF ) ) with typecode |-
9	4 8	syl5	Could not format ( Rel R -> ( ( dom R e. HF /\ ran R e. HF ) -> R e. HF ) ) : No typesetting found for |- ( Rel R -> ( ( dom R e. HF /\ ran R e. HF ) -> R e. HF ) ) with typecode |-
10	3 9	impbid2	Could not format ( Rel R -> ( R e. HF <-> ( dom R e. HF /\ ran R e. HF ) ) ) : No typesetting found for |- ( Rel R -> ( R e. HF <-> ( dom R e. HF /\ ran R e. HF ) ) ) with typecode |-