r1omhfb

Description: The class of all hereditarily finite sets is the only class with the property that all sets are members of it iff they are finite and all of their elements are members of it. (Contributed by BTernaryTau, 24-Jan-2026)

		Ref	Expression
	Assertion	r1omhfb	$⊢ H = ⋃ R_{1} [ω] \leftrightarrow \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H))$

Proof

Step	Hyp	Ref	Expression
1		r1omhf	$⊢ x \in ⋃ R_{1} [ω] \leftrightarrow (x \in Fin \land \forall y \in x y \in ⋃ R_{1} [ω])$
2		eleq2w2	$⊢ H = ⋃ R_{1} [ω] \to (x \in H \leftrightarrow x \in ⋃ R_{1} [ω])$
3		eleq2w2	$⊢ H = ⋃ R_{1} [ω] \to (y \in H \leftrightarrow y \in ⋃ R_{1} [ω])$
4	3	ralbidv	$⊢ H = ⋃ R_{1} [ω] \to (\forall y \in x y \in H \leftrightarrow \forall y \in x y \in ⋃ R_{1} [ω])$
5	4	anbi2d	$⊢ H = ⋃ R_{1} [ω] \to ((x \in Fin \land \forall y \in x y \in H) \leftrightarrow (x \in Fin \land \forall y \in x y \in ⋃ R_{1} [ω]))$
6	2 5	bibi12d	$⊢ H = ⋃ R_{1} [ω] \to ((x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \leftrightarrow (x \in ⋃ R_{1} [ω] \leftrightarrow (x \in Fin \land \forall y \in x y \in ⋃ R_{1} [ω])))$
7	1 6	mpbiri	$⊢ H = ⋃ R_{1} [ω] \to (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H))$
8	7	alrimiv	$⊢ H = ⋃ R_{1} [ω] \to \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H))$
9		biimp	$⊢ (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to (x \in H \to (x \in Fin \land \forall y \in x y \in H))$
10	9	alimi	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H))$
11		simpr	$⊢ (x \in Fin \land \forall y \in x y \in H) \to \forall y \in x y \in H$
12	11	imim2i	$⊢ (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to (x \in H \to \forall y \in x y \in H)$
13	12	alimi	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to \forall x (x \in H \to \forall y \in x y \in H)$
14	13	ralrid	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to \forall x \in H \forall y \in x y \in H$
15		dftr5	$⊢ Tr H \leftrightarrow \forall x \in H \forall y \in x y \in H$
16	14 15	sylibr	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to Tr H$
17		simpl	$⊢ (x \in Fin \land \forall y \in x y \in H) \to x \in Fin$
18	17	imim2i	$⊢ (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to (x \in H \to x \in Fin)$
19	18	alimi	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to \forall x (x \in H \to x \in Fin)$
20		df-ss	$⊢ H \subseteq Fin \leftrightarrow \forall x (x \in H \to x \in Fin)$
21	19 20	sylibr	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq Fin$
22		trssfir1om	$⊢ (Tr H \land H \subseteq Fin) \to H \subseteq ⋃ R_{1} [ω]$
23	16 21 22	syl2anc	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq ⋃ R_{1} [ω]$
24	10 23	syl	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq ⋃ R_{1} [ω]$
25		biimpr	$⊢ (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to ((x \in Fin \land \forall y \in x y \in H) \to x \in H)$
26	25	alimi	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H)$
27		eleq1w	$⊢ z = w \to (z \in ⋃ R_{1} [ω] \leftrightarrow w \in ⋃ R_{1} [ω])$
28		eleq1w	$⊢ z = w \to (z \in H \leftrightarrow w \in H)$
29	27 28	imbi12d	$⊢ z = w \to ((z \in ⋃ R_{1} [ω] \to z \in H) \leftrightarrow (w \in ⋃ R_{1} [ω] \to w \in H))$
30	29	imbi2d	$⊢ z = w \to ((\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (z \in ⋃ R_{1} [ω] \to z \in H)) \leftrightarrow (\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (w \in ⋃ R_{1} [ω] \to w \in H)))$
31		ra4v	$⊢ \forall w \in z (\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (w \in ⋃ R_{1} [ω] \to w \in H)) \to (\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to \forall w \in z (w \in ⋃ R_{1} [ω] \to w \in H))$
32		r1omhf	$⊢ z \in ⋃ R_{1} [ω] \leftrightarrow (z \in Fin \land \forall w \in z w \in ⋃ R_{1} [ω])$
33		ralim	$⊢ \forall w \in z (w \in ⋃ R_{1} [ω] \to w \in H) \to (\forall w \in z w \in ⋃ R_{1} [ω] \to \forall w \in z w \in H)$
34	33	anim2d	$⊢ \forall w \in z (w \in ⋃ R_{1} [ω] \to w \in H) \to ((z \in Fin \land \forall w \in z w \in ⋃ R_{1} [ω]) \to (z \in Fin \land \forall w \in z w \in H))$
35	32 34	biimtrid	$⊢ \forall w \in z (w \in ⋃ R_{1} [ω] \to w \in H) \to (z \in ⋃ R_{1} [ω] \to (z \in Fin \land \forall w \in z w \in H))$
36		eleq1w	$⊢ x = z \to (x \in Fin \leftrightarrow z \in Fin)$
37		eleq1w	$⊢ y = w \to (y \in H \leftrightarrow w \in H)$
38	37	adantl	$⊢ (x = z \land y = w) \to (y \in H \leftrightarrow w \in H)$
39		simpl	$⊢ (x = z \land y = w) \to x = z$
40	38 39	cbvraldva2	$⊢ x = z \to (\forall y \in x y \in H \leftrightarrow \forall w \in z w \in H)$
41	36 40	anbi12d	$⊢ x = z \to ((x \in Fin \land \forall y \in x y \in H) \leftrightarrow (z \in Fin \land \forall w \in z w \in H))$
42		eleq1w	$⊢ x = z \to (x \in H \leftrightarrow z \in H)$
43	41 42	imbi12d	$⊢ x = z \to (((x \in Fin \land \forall y \in x y \in H) \to x \in H) \leftrightarrow ((z \in Fin \land \forall w \in z w \in H) \to z \in H))$
44	43	spvv	$⊢ \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to ((z \in Fin \land \forall w \in z w \in H) \to z \in H)$
45	35 44	syl9r	$⊢ \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (\forall w \in z (w \in ⋃ R_{1} [ω] \to w \in H) \to (z \in ⋃ R_{1} [ω] \to z \in H))$
46	31 45	sylcom	$⊢ \forall w \in z (\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (w \in ⋃ R_{1} [ω] \to w \in H)) \to (\forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (z \in ⋃ R_{1} [ω] \to z \in H))$
47	30 46	setinds2	$⊢ \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to (z \in ⋃ R_{1} [ω] \to z \in H)$
48	47	ssrdv	$⊢ \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to ⋃ R_{1} [ω] \subseteq H$
49	26 48	syl	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to ⋃ R_{1} [ω] \subseteq H$
50	24 49	eqssd	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to H = ⋃ R_{1} [ω]$
51	8 50	impbii	$⊢ H = ⋃ R_{1} [ω] \leftrightarrow \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H))$

Metamath Proof Explorer

Theorem r1omhfb

Proof