Metamath Proof Explorer

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 ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ HF )

Proof

Step Hyp Ref Expression
1 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
2 1 3anbi1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) ↔ ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) ) )
3 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ HF ↔ 𝑦 ∈ HF ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ HF ) ↔ ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ HF ) ) )
5 ssel2 ⊢ ( ( 𝐴 ⊆ Fin ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ Fin )
6 5 ancoms ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ Fin )
7 6 3adant2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ Fin )
8 7 a1i ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ HF ) → ( ( 𝑥 ∈ 𝐴 ∧ 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 ) → 𝑦 ∈ HF ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ HF ) )
20 18 19 syl5 ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ HF ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ HF ) )
21 8 20 jcad ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ HF ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ HF ) ) )
22 elhf4 ⊢ ( 𝑥 ∈ HF ↔ ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ HF ) )
23 21 22 imbitrrdi ⊢ ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑦 ∈ HF ) → ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ HF ) )
24 4 23 setinds2regs ⊢ ( ( 𝑥 ∈ 𝐴 ∧ Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ HF )
25 24 3expib ⊢ ( 𝑥 ∈ 𝐴 → ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝑥 ∈ HF ) )
26 25 com12 ⊢ ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ HF ) )
27 26 ssrdv ⊢ ( ( Tr 𝐴 ∧ 𝐴 ⊆ Fin ) → 𝐴 ⊆ HF )