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 𝐴 → Tr Scott 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		r1tr	⊢ Tr ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) )
2		trin	⊢ ( ( Tr 𝐴 ∧ Tr ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) → Tr ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) )
3	1 2	mpan2	⊢ ( Tr 𝐴 → Tr ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) )
4		dfscott3	⊢ Scott 𝐴 = ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) )
5		treq	⊢ ( Scott 𝐴 = ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) → ( Tr Scott 𝐴 ↔ Tr ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) ) )
6	4 5	ax-mp	⊢ ( Tr Scott 𝐴 ↔ Tr ( 𝐴 ∩ ( 𝑅1 ‘ suc ∩ ( rank “ 𝐴 ) ) ) )
7	3 6	sylibr	⊢ ( Tr 𝐴 → Tr Scott 𝐴 )