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 \in Hf \leftrightarrow (A \in Fin \land A \subseteq Hf)$

Proof

Step	Hyp	Ref	Expression
1		hffi	$⊢ A \in Hf \to A \in Fin$
2		hfelhf	$⊢ (x \in A \land A \in Hf) \to x \in Hf$
3	2	expcom	$⊢ A \in Hf \to (x \in A \to x \in Hf)$
4	3	ssrdv	$⊢ A \in Hf \to A \subseteq Hf$
5	1 4	jca	$⊢ A \in Hf \to (A \in Fin \land A \subseteq Hf)$
6		eleq1	$⊢ x = \emptyset \to (x \in Hf \leftrightarrow \emptyset \in Hf)$
7		eleq1	$⊢ x = y \to (x \in Hf \leftrightarrow y \in Hf)$
8		eleq1	$⊢ x = y \cup \{z\} \to (x \in Hf \leftrightarrow y \cup \{z\} \in Hf)$
9		eleq1	$⊢ x = A \to (x \in Hf \leftrightarrow A \in Hf)$
10		0hf	$⊢ \emptyset \in Hf$
11	10	a1i	$⊢ (A \in Fin \land A \subseteq Hf) \to \emptyset \in Hf$
12		eldifi	$⊢ z \in (A ∖ y) \to z \in A$
13		ssel2	$⊢ (A \subseteq Hf \land z \in A) \to z \in Hf$
14	12 13	sylan2	$⊢ (A \subseteq Hf \land z \in (A ∖ y)) \to z \in Hf$
15		hfadj	$⊢ (y \in Hf \land z \in Hf) \to y \cup \{z\} \in Hf$
16	15	expcom	$⊢ z \in Hf \to (y \in Hf \to y \cup \{z\} \in Hf)$
17	14 16	syl	$⊢ (A \subseteq Hf \land z \in (A ∖ y)) \to (y \in Hf \to y \cup \{z\} \in Hf)$
18	17	ad2ant2l	$⊢ ((A \in Fin \land A \subseteq Hf) \land (y \subseteq A \land z \in (A ∖ y))) \to (y \in Hf \to y \cup \{z\} \in Hf)$
19		simpl	$⊢ (A \in Fin \land A \subseteq Hf) \to A \in Fin$
20	6 7 8 9 11 18 19	findcard2d	$⊢ (A \in Fin \land A \subseteq Hf) \to A \in Hf$
21	5 20	impbii	$⊢ A \in Hf \leftrightarrow (A \in Fin \land A \subseteq Hf)$

Metamath Proof Explorer

Theorem elhf3

Proof