Theorem dfscott2

Description: Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026)

	Ref	Expression
Assertion	dfscott2	$$⊢ScottA=\left\{x\in A|\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-scott	$$⊢ScottA=\left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$
2		rankfn	$$⊢\mathrm{rank}Fn\mathrm{V}$$
3		ssv	$$⊢A\subseteq \mathrm{V}$$
4		fnfvintima	$$⊢\left(\mathrm{rank}Fn\mathrm{V}\wedge A\subseteq \mathrm{V}\wedge x\in A\right)\to \left(\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]\leftrightarrow \forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
5	2 3 4	mp3an12	$$⊢x\in A\to \left(\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]\leftrightarrow \forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right)$$
6	5	rabbiia	$$⊢\left\{x\in A|\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]\right\}=\left\{x\in A|\forall y\in A\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(y\right)\right\}$$
7	1 6	eqtr4i	$$⊢ScottA=\left\{x\in A|\mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]\right\}$$