trssfir1omregs

Description: If every element in a transitive class is finite, then every element is also hereditarily finite. (Contributed by BTernaryTau, 20-Jan-2026)

		Ref	Expression
	Assertion	trssfir1omregs	$⊢ (Tr A \land A \subseteq Fin) \to A \subseteq ⋃ R_{1} [ω]$

Proof

Step	Hyp	Ref	Expression
1		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
2	1	3anbi1d	$⊢ x = y \to ((x \in A \land Tr A \land A \subseteq Fin) \leftrightarrow (y \in A \land Tr A \land A \subseteq Fin))$
3		eleq1w	$⊢ x = y \to (x \in ⋃ R_{1} [ω] \leftrightarrow y \in ⋃ R_{1} [ω])$
4	2 3	imbi12d	$⊢ x = y \to (((x \in A \land Tr A \land A \subseteq Fin) \to x \in ⋃ R_{1} [ω]) \leftrightarrow ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]))$
5		ssel2	$⊢ (A \subseteq Fin \land x \in A) \to x \in Fin$
6	5	ancoms	$⊢ (x \in A \land A \subseteq Fin) \to x \in Fin$
7	6	3adant2	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to x \in Fin$
8	7	a1i	$⊢ \forall y \in x ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]) \to ((x \in A \land Tr A \land A \subseteq Fin) \to x \in Fin)$
9		trel	$⊢ Tr A \to ((y \in x \land x \in A) \to y \in A)$
10	9	expcomd	$⊢ Tr A \to (x \in A \to (y \in x \to y \in A))$
11	10	impcom	$⊢ (x \in A \land Tr A) \to (y \in x \to y \in A)$
12	11	3adant3	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to (y \in x \to y \in A)$
13		simp2	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to Tr A$
14	13	a1d	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to (y \in x \to Tr A)$
15		simp3	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to A \subseteq Fin$
16	15	a1d	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to (y \in x \to A \subseteq Fin)$
17	12 14 16	3jcad	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to (y \in x \to (y \in A \land Tr A \land A \subseteq Fin))$
18	17	ralrimiv	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to \forall y \in x (y \in A \land Tr A \land A \subseteq Fin)$
19		ralim	$⊢ \forall y \in x ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]) \to (\forall y \in x (y \in A \land Tr A \land A \subseteq Fin) \to \forall y \in x y \in ⋃ R_{1} [ω])$
20	18 19	syl5	$⊢ \forall y \in x ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]) \to ((x \in A \land Tr A \land A \subseteq Fin) \to \forall y \in x y \in ⋃ R_{1} [ω])$
21	8 20	jcad	$⊢ \forall y \in x ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]) \to ((x \in A \land Tr A \land A \subseteq Fin) \to (x \in Fin \land \forall y \in x y \in ⋃ R_{1} [ω]))$
22		r1omhf	$⊢ x \in ⋃ R_{1} [ω] \leftrightarrow (x \in Fin \land \forall y \in x y \in ⋃ R_{1} [ω])$
23	21 22	imbitrrdi	$⊢ \forall y \in x ((y \in A \land Tr A \land A \subseteq Fin) \to y \in ⋃ R_{1} [ω]) \to ((x \in A \land Tr A \land A \subseteq Fin) \to x \in ⋃ R_{1} [ω])$
24	4 23	setinds2regs	$⊢ (x \in A \land Tr A \land A \subseteq Fin) \to x \in ⋃ R_{1} [ω]$
25	24	3expib	$⊢ x \in A \to ((Tr A \land A \subseteq Fin) \to x \in ⋃ R_{1} [ω])$
26	25	com12	$⊢ (Tr A \land A \subseteq Fin) \to (x \in A \to x \in ⋃ R_{1} [ω])$
27	26	ssrdv	$⊢ (Tr A \land A \subseteq Fin) \to A \subseteq ⋃ R_{1} [ω]$

Metamath Proof Explorer

Theorem trssfir1omregs

Proof