r1omhfbregs

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, 21-Jan-2026)

		Ref	Expression
	Assertion	r1omhfbregs	$⊢ 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		df-ral	$⊢ \forall x \in H \forall y \in x y \in H \leftrightarrow \forall x (x \in H \to \forall y \in x y \in H)$
15	13 14	sylibr	$⊢ \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$
16		dftr5	$⊢ Tr H \leftrightarrow \forall x \in H \forall y \in x y \in H$
17	15 16	sylibr	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to Tr H$
18		simpl	$⊢ (x \in Fin \land \forall y \in x y \in H) \to x \in Fin$
19	18	imim2i	$⊢ (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to (x \in H \to x \in Fin)$
20	19	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)$
21		df-ss	$⊢ H \subseteq Fin \leftrightarrow \forall x (x \in H \to x \in Fin)$
22	20 21	sylibr	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq Fin$
23		trssfir1omregs	$⊢ (Tr H \land H \subseteq Fin) \to H \subseteq ⋃ R_{1} [ω]$
24	17 22 23	syl2anc	$⊢ \forall x (x \in H \to (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq ⋃ R_{1} [ω]$
25	10 24	syl	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to H \subseteq ⋃ R_{1} [ω]$
26		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)$
27	26	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)$
28		eleq1w	$⊢ z = w \to (z \in ⋃ R_{1} [ω] \leftrightarrow w \in ⋃ R_{1} [ω])$
29		eleq1w	$⊢ z = w \to (z \in H \leftrightarrow w \in H)$
30	28 29	imbi12d	$⊢ z = w \to ((z \in ⋃ R_{1} [ω] \to z \in H) \leftrightarrow (w \in ⋃ R_{1} [ω] \to w \in H))$
31	30	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)))$
32		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))$
33		r1omhf	$⊢ z \in ⋃ R_{1} [ω] \leftrightarrow (z \in Fin \land \forall w \in z w \in ⋃ R_{1} [ω])$
34		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)$
35	34	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))$
36	33 35	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))$
37		eleq1w	$⊢ x = z \to (x \in Fin \leftrightarrow z \in Fin)$
38		eleq1w	$⊢ y = w \to (y \in H \leftrightarrow w \in H)$
39	38	adantl	$⊢ (x = z \land y = w) \to (y \in H \leftrightarrow w \in H)$
40		simpl	$⊢ (x = z \land y = w) \to x = z$
41	39 40	cbvraldva2	$⊢ x = z \to (\forall y \in x y \in H \leftrightarrow \forall w \in z w \in H)$
42	37 41	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))$
43		eleq1w	$⊢ x = z \to (x \in H \leftrightarrow z \in H)$
44	42 43	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))$
45	44	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)$
46	36 45	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))$
47	32 46	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))$
48	31 47	setinds2regs	$⊢ \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)$
49	48	ssrdv	$⊢ \forall x ((x \in Fin \land \forall y \in x y \in H) \to x \in H) \to ⋃ R_{1} [ω] \subseteq H$
50	27 49	syl	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to ⋃ R_{1} [ω] \subseteq H$
51	25 50	eqssd	$⊢ \forall x (x \in H \leftrightarrow (x \in Fin \land \forall y \in x y \in H)) \to H = ⋃ R_{1} [ω]$
52	8 51	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 r1omhfbregs

Proof