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	⊢ ( 𝐴 ∈ Hf ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) )

Proof

Step	Hyp	Ref	Expression
1		hffi	⊢ ( 𝐴 ∈ Hf → 𝐴 ∈ Fin )
2		hfelhf	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ∈ Hf ) → 𝑥 ∈ Hf )
3	2	expcom	⊢ ( 𝐴 ∈ Hf → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ Hf ) )
4	3	ssrdv	⊢ ( 𝐴 ∈ Hf → 𝐴 ⊆ Hf )
5	1 4	jca	⊢ ( 𝐴 ∈ Hf → ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) )
6		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ Hf ↔ ∅ ∈ Hf ) )
7		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ Hf ↔ 𝑦 ∈ Hf ) )
8		eleq1	⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∈ Hf ↔ ( 𝑦 ∪ { 𝑧 } ) ∈ Hf ) )
9		eleq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ Hf ↔ 𝐴 ∈ Hf ) )
10		0hf	⊢ ∅ ∈ Hf
11	10	a1i	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) → ∅ ∈ Hf )
12		eldifi	⊢ ( 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) → 𝑧 ∈ 𝐴 )
13		ssel2	⊢ ( ( 𝐴 ⊆ Hf ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ Hf )
14	12 13	sylan2	⊢ ( ( 𝐴 ⊆ Hf ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → 𝑧 ∈ Hf )
15		hfadj	⊢ ( ( 𝑦 ∈ Hf ∧ 𝑧 ∈ Hf ) → ( 𝑦 ∪ { 𝑧 } ) ∈ Hf )
16	15	expcom	⊢ ( 𝑧 ∈ Hf → ( 𝑦 ∈ Hf → ( 𝑦 ∪ { 𝑧 } ) ∈ Hf ) )
17	14 16	syl	⊢ ( ( 𝐴 ⊆ Hf ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) → ( 𝑦 ∈ Hf → ( 𝑦 ∪ { 𝑧 } ) ∈ Hf ) )
18	17	ad2ant2l	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑧 ∈ ( 𝐴 ∖ 𝑦 ) ) ) → ( 𝑦 ∈ Hf → ( 𝑦 ∪ { 𝑧 } ) ∈ Hf ) )
19		simpl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) → 𝐴 ∈ Fin )
20	6 7 8 9 11 18 19	findcard2d	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) → 𝐴 ∈ Hf )
21	5 20	impbii	⊢ ( 𝐴 ∈ Hf ↔ ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ Hf ) )