Theorem elhf4

Description: A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026) Use HF . (Revised by BTernaryTau, 17-Sep-2026)

	Ref	Expression
Assertion	elhf4	Could not format assertion : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hffi	Could not format ( A e. HF -> A e. Fin ) : No typesetting found for |- ( A e. HF -> A e. Fin ) with typecode |-
2		r1tr	$$⊢\mathrm{Tr}{R}_1\left(y\right)$$
3		trel	$$⊢\mathrm{Tr}{R}_1\left(y\right)\to \left(\left(x\in A\wedge A\in R_1\left(y\right)\right)\to x\in R_1\left(y\right)\right)$$
4	2 3	ax-mp	$$⊢\left(x\in A\wedge A\in R_1\left(y\right)\right)\to x\in R_1\left(y\right)$$
5	4	ex	$$⊢x\in A\to \left(A\in R_1\left(y\right)\to x\in R_1\left(y\right)\right)$$
6	5	reximdv	$$⊢x\in A\to \left(\exists y\in \mathrm{\omega }A\in R_1\left(y\right)\to \exists y\in \mathrm{\omega }x\in R_1\left(y\right)\right)$$
7		elhf	Could not format ( A e. HF <-> E. y e. _om A e. ( R1 ` y ) ) : No typesetting found for |- ( A e. HF <-> E. y e. _om A e. ( R1 ` y ) ) with typecode |-
8		elhf	Could not format ( x e. HF <-> E. y e. _om x e. ( R1 ` y ) ) : No typesetting found for |- ( x e. HF <-> E. y e. _om x e. ( R1 ` y ) ) with typecode |-
9	6 7 8	3imtr4g	Could not format ( x e. A -> ( A e. HF -> x e. HF ) ) : No typesetting found for |- ( x e. A -> ( A e. HF -> x e. HF ) ) with typecode |-
10	9	com12	Could not format ( A e. HF -> ( x e. A -> x e. HF ) ) : No typesetting found for |- ( A e. HF -> ( x e. A -> x e. HF ) ) with typecode |-
11	10	ralrimiv	Could not format ( A e. HF -> A. x e. A x e. HF ) : No typesetting found for |- ( A e. HF -> A. x e. A x e. HF ) with typecode |-
12	1 11	jca	Could not format ( A e. HF -> ( A e. Fin /\ A. x e. A x e. HF ) ) : No typesetting found for |- ( A e. HF -> ( A e. Fin /\ A. x e. A x e. HF ) ) with typecode |-
13		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for |- HF = U. ( R1 " _om ) with typecode |-
14	13	eleq2i	Could not format ( x e. HF <-> x e. U. ( R1 " _om ) ) : No typesetting found for |- ( x e. HF <-> x e. U. ( R1 " _om ) ) with typecode |-
15	14	ralbii	Could not format ( A. x e. A x e. HF <-> A. x e. A x e. U. ( R1 " _om ) ) : No typesetting found for |- ( A. x e. A x e. HF <-> A. x e. A x e. U. ( R1 " _om ) ) with typecode |-
16		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
17		r1filimi	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in Ax\in \bigcup R_1\left[\mathrm{\omega }\right]\wedge \mathrm{Lim}\mathrm{\omega }\right)\to A\in \bigcup R_1\left[\mathrm{\omega }\right]$$
18	16 17	mp3an3	$$⊢\left(A\in \mathrm{Fin}\wedge \forall x\in Ax\in \bigcup R_1\left[\mathrm{\omega }\right]\right)\to A\in \bigcup R_1\left[\mathrm{\omega }\right]$$
19	18 13	eleqtrrdi	Could not format ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) -> A e. HF ) : No typesetting found for |- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) -> A e. HF ) with typecode |-
20	15 19	sylan2b	Could not format ( ( A e. Fin /\ A. x e. A x e. HF ) -> A e. HF ) : No typesetting found for |- ( ( A e. Fin /\ A. x e. A x e. HF ) -> A e. HF ) with typecode |-
21	12 20	impbii	Could not format ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) ) : No typesetting found for |- ( A e. HF <-> ( A e. Fin /\ A. x e. A x e. HF ) ) with typecode |-