Metamath Proof Explorer

Theorem trscott

Description: The Scott's trick set of a transitive class is also transitive. (Contributed by BTernaryTau, 20-Oct-2026)

Ref Expression
Assertion trscott ⊢ Tr ⁡ A → Tr ⁡ Scott A

Proof

Step Hyp Ref Expression
1 r1tr ⊢ Tr ⁡ R1 ⁡ suc ⁡ ⋂ rank A
2 trin ⊢ Tr ⁡ A ∧ Tr ⁡ R1 ⁡ suc ⁡ ⋂ rank A → Tr ⁡ A ∩ R1 ⁡ suc ⁡ ⋂ rank A
3 1 2 mpan2 ⊢ Tr ⁡ A → Tr ⁡ A ∩ R1 ⁡ suc ⁡ ⋂ rank A
4 dfscott3 ⊢ Scott A = A ∩ R1 ⁡ suc ⁡ ⋂ rank A
5 treq ⊢ Scott A = A ∩ R1 ⁡ suc ⁡ ⋂ rank A → Tr ⁡ Scott A ↔ Tr ⁡ A ∩ R1 ⁡ suc ⁡ ⋂ rank A
6 4 5 ax-mp ⊢ Tr ⁡ Scott A ↔ Tr ⁡ A ∩ R1 ⁡ suc ⁡ ⋂ rank A
7 3 6 sylibr ⊢ Tr ⁡ A → Tr ⁡ Scott A