r1omhf

Description: A set is hereditarily finite iff it is finite and all of its elements are hereditarily finite. (Contributed by BTernaryTau, 19-Jan-2026)

		Ref	Expression
	Assertion	r1omhf	$⊢ A \in ⋃ R_{1} [ω] \leftrightarrow (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω])$

Proof

Step	Hyp	Ref	Expression
1		r1omfi	$⊢ ⋃ R_{1} [ω] \subseteq Fin$
2	1	sseli	$⊢ A \in ⋃ R_{1} [ω] \to A \in Fin$
3		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
4	3	simpli	$⊢ Fun R_{1}$
5		eluniima	$⊢ Fun R_{1} \to (A \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω A \in R_{1} (y))$
6	4 5	ax-mp	$⊢ A \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω A \in R_{1} (y)$
7		r19.41v	$⊢ \exists y \in ω (A \in R_{1} (y) \land x \in A) \leftrightarrow (\exists y \in ω A \in R_{1} (y) \land x \in A)$
8		r1elcl	$⊢ (A \in R_{1} (y) \land x \in A) \to x \in R_{1} (y)$
9	8	reximi	$⊢ \exists y \in ω (A \in R_{1} (y) \land x \in A) \to \exists y \in ω x \in R_{1} (y)$
10	7 9	sylbir	$⊢ (\exists y \in ω A \in R_{1} (y) \land x \in A) \to \exists y \in ω x \in R_{1} (y)$
11	6 10	sylanb	$⊢ (A \in ⋃ R_{1} [ω] \land x \in A) \to \exists y \in ω x \in R_{1} (y)$
12		eluniima	$⊢ Fun R_{1} \to (x \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω x \in R_{1} (y))$
13	4 12	ax-mp	$⊢ x \in ⋃ R_{1} [ω] \leftrightarrow \exists y \in ω x \in R_{1} (y)$
14	11 13	sylibr	$⊢ (A \in ⋃ R_{1} [ω] \land x \in A) \to x \in ⋃ R_{1} [ω]$
15	14	ralrimiva	$⊢ A \in ⋃ R_{1} [ω] \to \forall x \in A x \in ⋃ R_{1} [ω]$
16	2 15	jca	$⊢ A \in ⋃ R_{1} [ω] \to (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω])$
17		limom	$⊢ Lim ω$
18		r1filimi	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω] \land Lim ω) \to A \in ⋃ R_{1} [ω]$
19	17 18	mp3an3	$⊢ (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω]) \to A \in ⋃ R_{1} [ω]$
20	16 19	impbii	$⊢ A \in ⋃ R_{1} [ω] \leftrightarrow (A \in Fin \land \forall x \in A x \in ⋃ R_{1} [ω])$

Metamath Proof Explorer

Theorem r1omhf

Proof