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 i^i ( R1 ` suc |^| ( rank " A ) ) ) )
3	1 2	mpan2	|- ( Tr A -> Tr ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) )
4		dfscott3	|- Scott A = ( A i^i ( R1 ` suc |^| ( rank " A ) ) )
5		treq	|- ( Scott A = ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) -> ( Tr Scott A <-> Tr ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) ) )
6	4 5	ax-mp	|- ( Tr Scott A <-> Tr ( A i^i ( R1 ` suc |^| ( rank " A ) ) ) )
7	3 6	sylibr	|- ( Tr A -> Tr Scott A )