Theorem trssfihfregs

Description: If every element in a transitive class is finite, then every element is also hereditarily finite. This version of trssfihf replaces setinds2 with setinds2regs . (Contributed by BTernaryTau, 20-Jan-2026) Use HF . (Revised by BTernaryTau, 24-Oct-2026)

	Ref	Expression
Assertion	trssfihfregs	Could not format assertion : No typesetting found for |- ( ( Tr A /\ A C_ Fin ) -> A C_ HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$$⊢x=y\to \left(x\in A\leftrightarrow y\in A\right)$$
2	1	3anbi1d	$$⊢x=y\to \left(\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\leftrightarrow \left(y\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\right)$$
3		eleq1w	Could not format ( x = y -> ( x e. HF <-> y e. HF ) ) : No typesetting found for |- ( x = y -> ( x e. HF <-> y e. HF ) ) with typecode |-
4	2 3	imbi12d	Could not format ( x = y -> ( ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) <-> ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) ) ) : No typesetting found for |- ( x = y -> ( ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) <-> ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) ) ) with typecode |-
5		ssel2	$$⊢\left(A\subseteq \mathrm{Fin}\wedge x\in A\right)\to x\in \mathrm{Fin}$$
6	5	ancoms	$$⊢\left(x\in A\wedge A\subseteq \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
7	6	3adant2	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to x\in \mathrm{Fin}$$
8	7	a1i	Could not format ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. Fin ) ) : No typesetting found for |- ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. Fin ) ) with typecode |-
9		trel	$$⊢\mathrm{Tr}A\to \left(\left(y\in x\wedge x\in A\right)\to y\in A\right)$$
10	9	expcomd	$$⊢\mathrm{Tr}A\to \left(x\in A\to \left(y\in x\to y\in A\right)\right)$$
11	10	impcom	$$⊢\left(x\in A\wedge \mathrm{Tr}A\right)\to \left(y\in x\to y\in A\right)$$
12	11	3adant3	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \left(y\in x\to y\in A\right)$$
13		simp2	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \mathrm{Tr}A$$
14	13	a1d	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \left(y\in x\to \mathrm{Tr}A\right)$$
15		simp3	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to A\subseteq \mathrm{Fin}$$
16	15	a1d	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \left(y\in x\to A\subseteq \mathrm{Fin}\right)$$
17	12 14 16	3jcad	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \left(y\in x\to \left(y\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\right)$$
18	17	ralrimiv	$$⊢\left(x\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)\to \forall y\in x\left(y\in A\wedge \mathrm{Tr}A\wedge A\subseteq \mathrm{Fin}\right)$$
19		ralim	Could not format ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( A. y e. x ( y e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. HF ) ) : No typesetting found for |- ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( A. y e. x ( y e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. HF ) ) with typecode |-
20	18 19	syl5	Could not format ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. HF ) ) : No typesetting found for |- ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> A. y e. x y e. HF ) ) with typecode |-
21	8 20	jcad	Could not format ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( x e. Fin /\ A. y e. x y e. HF ) ) ) : No typesetting found for |- ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> ( x e. Fin /\ A. y e. x y e. HF ) ) ) with typecode |-
22		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 |-
23	21 22	imbitrrdi	Could not format ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) ) : No typesetting found for |- ( A. y e. x ( ( y e. A /\ Tr A /\ A C_ Fin ) -> y e. HF ) -> ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) ) with typecode |-
24	4 23	setinds2regs	Could not format ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) : No typesetting found for |- ( ( x e. A /\ Tr A /\ A C_ Fin ) -> x e. HF ) with typecode |-
25	24	3expib	Could not format ( x e. A -> ( ( Tr A /\ A C_ Fin ) -> x e. HF ) ) : No typesetting found for |- ( x e. A -> ( ( Tr A /\ A C_ Fin ) -> x e. HF ) ) with typecode |-
26	25	com12	Could not format ( ( Tr A /\ A C_ Fin ) -> ( x e. A -> x e. HF ) ) : No typesetting found for |- ( ( Tr A /\ A C_ Fin ) -> ( x e. A -> x e. HF ) ) with typecode |-
27	26	ssrdv	Could not format ( ( Tr A /\ A C_ Fin ) -> A C_ HF ) : No typesetting found for |- ( ( Tr A /\ A C_ Fin ) -> A C_ HF ) with typecode |-