Metamath Proof Explorer

Theorem 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 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ ∪ ( 𝑅1 “ ω ) )

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
2 1 3anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) ↔ ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) ) )
5 ssel2 ⊢ ( ( 𝐴 ⊆ Fin ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Fin )
6 5 ancoms ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ Fin )
7 6 3adant2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ Fin )
8 7 a1i ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ Fin ) )
9 trel ⊢ ( Tr 𝐴 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 ) )
10 9 expcomd ⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) ) )
11 10 impcom ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) )
12 11 3adant3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐴 ) )
13 simp2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → Tr 𝐴 )
14 13 a1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑦 ∈ 𝑥 → Tr 𝐴 ) )
15 simp3 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ Fin )
16 15 a1d ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑦 ∈ 𝑥 → 𝐴 ⊆ Fin ) )
17 12 14 16 3jcad ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑦 ∈ 𝑥 → ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) ) )
18 17 ralrimiv ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) )
19 ralim ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
20 18 19 syl5 ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
21 8 20 jcad ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) ) )
22 r1omhf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) )
23 21 22 imbitrrdi ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )
24 4 23 setinds2regs ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) )
25 24 3expib ⊢ ( 𝑥 ∈ 𝐴 → ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )
26 25 com12 ⊢ ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ( 𝑅1 “ ω ) ) )
27 26 ssrdv ⊢ ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ ∪ ( 𝑅1 “ ω ) )