Theorem eqhfregs

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. This version of eqhf replaces setinds2 with setinds2regs and trssfihf with trssfihfregs . (Contributed by BTernaryTau, 21-Jan-2026) Use HF . (Revised by BTernaryTau, 24-Oct-2026)

	Ref	Expression
Assertion	eqhfregs	Could not format assertion : No typesetting found for |- ( H = HF <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elhf4	Could not format ( x e. HF <-> ( x e. Fin /\ A. y e. x y e. HF ) ) : No typesetting found for |- ( x e. HF <-> ( x e. Fin /\ A. y e. x y e. HF ) ) with typecode |-
2		eleq2w2	Could not format ( H = HF -> ( x e. H <-> x e. HF ) ) : No typesetting found for |- ( H = HF -> ( x e. H <-> x e. HF ) ) with typecode |-
3		eleq2w2	Could not format ( H = HF -> ( y e. H <-> y e. HF ) ) : No typesetting found for |- ( H = HF -> ( y e. H <-> y e. HF ) ) with typecode |-
4	3	ralbidv	Could not format ( H = HF -> ( A. y e. x y e. H <-> A. y e. x y e. HF ) ) : No typesetting found for |- ( H = HF -> ( A. y e. x y e. H <-> A. y e. x y e. HF ) ) with typecode |-
5	4	anbi2d	Could not format ( H = HF -> ( ( x e. Fin /\ A. y e. x y e. H ) <-> ( x e. Fin /\ A. y e. x y e. HF ) ) ) : No typesetting found for |- ( H = HF -> ( ( x e. Fin /\ A. y e. x y e. H ) <-> ( x e. Fin /\ A. y e. x y e. HF ) ) ) with typecode |-
6	2 5	bibi12d	Could not format ( H = HF -> ( ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) <-> ( x e. HF <-> ( x e. Fin /\ A. y e. x y e. HF ) ) ) ) : No typesetting found for |- ( H = HF -> ( ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) <-> ( x e. HF <-> ( x e. Fin /\ A. y e. x y e. HF ) ) ) ) with typecode |-
7	1 6	mpbiri	Could not format ( H = HF -> ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) : No typesetting found for |- ( H = HF -> ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) with typecode |-
8	7	alrimiv	Could not format ( H = HF -> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) : No typesetting found for |- ( H = HF -> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) with typecode |-
9		biimp	$$⊢\left(x\in H\leftrightarrow \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)$$
10	9	alimi	$$⊢\forall x\left(x\in H\leftrightarrow \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)$$
11		simpr	$$⊢\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to \forall y\in xy\in H$$
12	11	imim2i	$$⊢\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \left(x\in H\to \forall y\in xy\in H\right)$$
13	12	alimi	$$⊢\forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \forall x\left(x\in H\to \forall y\in xy\in H\right)$$
14	13	ralrid	$$⊢\forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \forall x\in H\forall y\in xy\in H$$
15		dftr5	$$⊢\mathrm{Tr}H\leftrightarrow \forall x\in H\forall y\in xy\in H$$
16	14 15	sylibr	$$⊢\forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \mathrm{Tr}H$$
17		simpl	$$⊢\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to x\in \mathrm{Fin}$$
18	17	imim2i	$$⊢\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \left(x\in H\to x\in \mathrm{Fin}\right)$$
19	18	alimi	$$⊢\forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \forall x\left(x\in H\to x\in \mathrm{Fin}\right)$$
20		df-ss	$$⊢H\subseteq \mathrm{Fin}\leftrightarrow \forall x\left(x\in H\to x\in \mathrm{Fin}\right)$$
21	19 20	sylibr	$$⊢\forall x\left(x\in H\to \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to H\subseteq \mathrm{Fin}$$
22		trssfihfregs	Could not format ( ( Tr H /\ H C_ Fin ) -> H C_ HF ) : No typesetting found for |- ( ( Tr H /\ H C_ Fin ) -> H C_ HF ) with typecode |-
23	16 21 22	syl2anc	Could not format ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ HF ) : No typesetting found for |- ( A. x ( x e. H -> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ HF ) with typecode |-
24	10 23	syl	Could not format ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ HF ) : No typesetting found for |- ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H C_ HF ) with typecode |-
25		biimpr	$$⊢\left(x\in H\leftrightarrow \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \left(\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to x\in H\right)$$
26	25	alimi	$$⊢\forall x\left(x\in H\leftrightarrow \left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\right)\to \forall x\left(\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to x\in H\right)$$
27		eleq1w	Could not format ( z = w -> ( z e. HF <-> w e. HF ) ) : No typesetting found for |- ( z = w -> ( z e. HF <-> w e. HF ) ) with typecode |-
28		eleq1w	$$⊢z=w\to \left(z\in H\leftrightarrow w\in H\right)$$
29	27 28	imbi12d	Could not format ( z = w -> ( ( z e. HF -> z e. H ) <-> ( w e. HF -> w e. H ) ) ) : No typesetting found for |- ( z = w -> ( ( z e. HF -> z e. H ) <-> ( w e. HF -> w e. H ) ) ) with typecode |-
30	29	imbi2d	Could not format ( z = w -> ( ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) <-> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) ) ) : No typesetting found for |- ( z = w -> ( ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) <-> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) ) ) with typecode |-
31		ra4v	Could not format ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> A. w e. z ( w e. HF -> w e. H ) ) ) : No typesetting found for |- ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> A. w e. z ( w e. HF -> w e. H ) ) ) with typecode |-
32		elhf4	Could not format ( z e. HF <-> ( z e. Fin /\ A. w e. z w e. HF ) ) : No typesetting found for |- ( z e. HF <-> ( z e. Fin /\ A. w e. z w e. HF ) ) with typecode |-
33		ralim	Could not format ( A. w e. z ( w e. HF -> w e. H ) -> ( A. w e. z w e. HF -> A. w e. z w e. H ) ) : No typesetting found for |- ( A. w e. z ( w e. HF -> w e. H ) -> ( A. w e. z w e. HF -> A. w e. z w e. H ) ) with typecode |-
34	33	anim2d	Could not format ( A. w e. z ( w e. HF -> w e. H ) -> ( ( z e. Fin /\ A. w e. z w e. HF ) -> ( z e. Fin /\ A. w e. z w e. H ) ) ) : No typesetting found for |- ( A. w e. z ( w e. HF -> w e. H ) -> ( ( z e. Fin /\ A. w e. z w e. HF ) -> ( z e. Fin /\ A. w e. z w e. H ) ) ) with typecode |-
35	32 34	biimtrid	Could not format ( A. w e. z ( w e. HF -> w e. H ) -> ( z e. HF -> ( z e. Fin /\ A. w e. z w e. H ) ) ) : No typesetting found for |- ( A. w e. z ( w e. HF -> w e. H ) -> ( z e. HF -> ( z e. Fin /\ A. w e. z w e. H ) ) ) with typecode |-
36		eleq1w	$$⊢x=z\to \left(x\in \mathrm{Fin}\leftrightarrow z\in \mathrm{Fin}\right)$$
37		eleq1w	$$⊢y=w\to \left(y\in H\leftrightarrow w\in H\right)$$
38	37	adantl	$$⊢\left(x=z\wedge y=w\right)\to \left(y\in H\leftrightarrow w\in H\right)$$
39		simpl	$$⊢\left(x=z\wedge y=w\right)\to x=z$$
40	38 39	cbvraldva2	$$⊢x=z\to \left(\forall y\in xy\in H\leftrightarrow \forall w\in zw\in H\right)$$
41	36 40	anbi12d	$$⊢x=z\to \left(\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\leftrightarrow \left(z\in \mathrm{Fin}\wedge \forall w\in zw\in H\right)\right)$$
42		eleq1w	$$⊢x=z\to \left(x\in H\leftrightarrow z\in H\right)$$
43	41 42	imbi12d	$$⊢x=z\to \left(\left(\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to x\in H\right)\leftrightarrow \left(\left(z\in \mathrm{Fin}\wedge \forall w\in zw\in H\right)\to z\in H\right)\right)$$
44	43	spvv	$$⊢\forall x\left(\left(x\in \mathrm{Fin}\wedge \forall y\in xy\in H\right)\to x\in H\right)\to \left(\left(z\in \mathrm{Fin}\wedge \forall w\in zw\in H\right)\to z\in H\right)$$
45	35 44	syl9r	Could not format ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( A. w e. z ( w e. HF -> w e. H ) -> ( z e. HF -> z e. H ) ) ) : No typesetting found for |- ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( A. w e. z ( w e. HF -> w e. H ) -> ( z e. HF -> z e. H ) ) ) with typecode |-
46	31 45	sylcom	Could not format ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) ) : No typesetting found for |- ( A. w e. z ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( w e. HF -> w e. H ) ) -> ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) ) with typecode |-
47	30 46	setinds2regs	Could not format ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) : No typesetting found for |- ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> ( z e. HF -> z e. H ) ) with typecode |-
48	47	ssrdv	Could not format ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> HF C_ H ) : No typesetting found for |- ( A. x ( ( x e. Fin /\ A. y e. x y e. H ) -> x e. H ) -> HF C_ H ) with typecode |-
49	26 48	syl	Could not format ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> HF C_ H ) : No typesetting found for |- ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> HF C_ H ) with typecode |-
50	24 49	eqssd	Could not format ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H = HF ) : No typesetting found for |- ( A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) -> H = HF ) with typecode |-
51	8 50	impbii	Could not format ( H = HF <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) : No typesetting found for |- ( H = HF <-> A. x ( x e. H <-> ( x e. Fin /\ A. y e. x y e. H ) ) ) with typecode |-