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

Proof

Step	Hyp	Ref	Expression
1		hffi	$⊢ A \in Hf \to A \in Fin$
2		r1tr	$⊢ Tr R_{1} (y)$
3		trel	$⊢ Tr R_{1} (y) \to ((x \in A \land A \in R_{1} (y)) \to x \in R_{1} (y))$
4	2 3	ax-mp	$⊢ (x \in A \land A \in R_{1} (y)) \to x \in R_{1} (y)$
5	4	ex	$⊢ x \in A \to (A \in R_{1} (y) \to x \in R_{1} (y))$
6	5	reximdv	$⊢ x \in A \to (\exists y \in ω A \in R_{1} (y) \to \exists y \in ω x \in R_{1} (y))$
7		elhf	$⊢ A \in Hf \leftrightarrow \exists y \in ω A \in R_{1} (y)$
8		elhf	$⊢ x \in Hf \leftrightarrow \exists y \in ω x \in R_{1} (y)$
9	6 7 8	3imtr4g	$⊢ x \in A \to (A \in Hf \to x \in Hf)$
10	9	com12	$⊢ A \in Hf \to (x \in A \to x \in Hf)$
11	10	ralrimiv	$⊢ A \in Hf \to \forall x \in A x \in Hf$
12	1 11	jca	$⊢ A \in Hf \to (A \in Fin \land \forall x \in A x \in Hf)$
13		df-hf	$⊢ Hf = ⋃ R_{1} [ω]$
14	13	eleq2i	$⊢ x \in Hf \leftrightarrow x \in ⋃ R_{1} [ω]$
15	14	ralbii	$⊢ \forall x \in A x \in Hf \leftrightarrow \forall x \in A x \in ⋃ R_{1} [ω]$
16		limom	$⊢ Lim ω$
17		r1filimi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω] \land Lim ω) \to A \in ⋃ R_{1} [ω]$
18	16 17	mp3an3	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω]) \to A \in ⋃ R_{1} [ω]$
19	18 13	eleqtrrdi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω]) \to A \in Hf$
20	15 19	sylan2b	$⊢ (A \in Fin \land \forall x \in A x \in Hf) \to A \in Hf$
21	12 20	impbii	$⊢ A \in Hf \leftrightarrow (A \in Fin \land \forall x \in A x \in Hf)$

Metamath Proof Explorer

Theorem elhf4

Proof