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	|- ( A e. Hf <-> ( A e. Fin /\ A. x e. A x e. Hf ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	|- ( A e. Hf -> A e. Fin )
2		r1tr	|- Tr ( R1 ` y )
3		trel	|- ( Tr ( R1 ` y ) -> ( ( x e. A /\ A e. ( R1 ` y ) ) -> x e. ( R1 ` y ) ) )
4	2 3	ax-mp	|- ( ( x e. A /\ A e. ( R1 ` y ) ) -> x e. ( R1 ` y ) )
5	4	ex	|- ( x e. A -> ( A e. ( R1 ` y ) -> x e. ( R1 ` y ) ) )
6	5	reximdv	|- ( x e. A -> ( E. y e. _om A e. ( R1 ` y ) -> E. y e. _om x e. ( R1 ` y ) ) )
7		elhf	|- ( A e. Hf <-> E. y e. _om A e. ( R1 ` y ) )
8		elhf	|- ( x e. Hf <-> E. y e. _om x e. ( R1 ` y ) )
9	6 7 8	3imtr4g	|- ( x e. A -> ( A e. Hf -> x e. Hf ) )
10	9	com12	|- ( A e. Hf -> ( x e. A -> x e. Hf ) )
11	10	ralrimiv	|- ( A e. Hf -> A. x e. A x e. Hf )
12	1 11	jca	|- ( A e. Hf -> ( A e. Fin /\ A. x e. A x e. Hf ) )
13		df-hf	|- Hf = U. ( R1 " _om )
14	13	eleq2i	|- ( x e. Hf <-> x e. U. ( R1 " _om ) )
15	14	ralbii	|- ( A. x e. A x e. Hf <-> A. x e. A x e. U. ( R1 " _om ) )
16		limom	|- Lim _om
17		r1filimi	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) /\ Lim _om ) -> A e. U. ( R1 " _om ) )
18	16 17	mp3an3	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) -> A e. U. ( R1 " _om ) )
19	18 13	eleqtrrdi	|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " _om ) ) -> A e. Hf )
20	15 19	sylan2b	|- ( ( A e. Fin /\ A. x e. A x e. Hf ) -> A e. Hf )
21	12 20	impbii	|- ( A e. Hf <-> ( A e. Fin /\ A. x e. A x e. Hf ) )