Theorem elhf3

Description: A set is hereditarily finite if and only if it is finite and all its members are hereditarily finite. (Contributed by Eric Schmidt, 8-Sep-2026)

	Ref	Expression
Assertion	elhf3	|- ( A e. Hf <-> ( A e. Fin /\ A C_ Hf ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	|- ( A e. Hf -> A e. Fin )
2		hfelhf	|- ( ( x e. A /\ A e. Hf ) -> x e. Hf )
3	2	expcom	|- ( A e. Hf -> ( x e. A -> x e. Hf ) )
4	3	ssrdv	|- ( A e. Hf -> A C_ Hf )
5	1 4	jca	|- ( A e. Hf -> ( A e. Fin /\ A C_ Hf ) )
6		eleq1	|- ( x = (/) -> ( x e. Hf <-> (/) e. Hf ) )
7		eleq1	|- ( x = y -> ( x e. Hf <-> y e. Hf ) )
8		eleq1	|- ( x = ( y u. { z } ) -> ( x e. Hf <-> ( y u. { z } ) e. Hf ) )
9		eleq1	|- ( x = A -> ( x e. Hf <-> A e. Hf ) )
10		0hf	|- (/) e. Hf
11	10	a1i	|- ( ( A e. Fin /\ A C_ Hf ) -> (/) e. Hf )
12		eldifi	|- ( z e. ( A \ y ) -> z e. A )
13		ssel2	|- ( ( A C_ Hf /\ z e. A ) -> z e. Hf )
14	12 13	sylan2	|- ( ( A C_ Hf /\ z e. ( A \ y ) ) -> z e. Hf )
15		hfadj	|- ( ( y e. Hf /\ z e. Hf ) -> ( y u. { z } ) e. Hf )
16	15	expcom	|- ( z e. Hf -> ( y e. Hf -> ( y u. { z } ) e. Hf ) )
17	14 16	syl	|- ( ( A C_ Hf /\ z e. ( A \ y ) ) -> ( y e. Hf -> ( y u. { z } ) e. Hf ) )
18	17	ad2ant2l	|- ( ( ( A e. Fin /\ A C_ Hf ) /\ ( y C_ A /\ z e. ( A \ y ) ) ) -> ( y e. Hf -> ( y u. { z } ) e. Hf ) )
19		simpl	|- ( ( A e. Fin /\ A C_ Hf ) -> A e. Fin )
20	6 7 8 9 11 18 19	findcard2d	|- ( ( A e. Fin /\ A C_ Hf ) -> A e. Hf )
21	5 20	impbii	|- ( A e. Hf <-> ( A e. Fin /\ A C_ Hf ) )