Theorem rankscott

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

	Ref	Expression
Assertion	rankscott	⊢ ( 𝐴 ≠ ∅ → ( rank ‘ Scott 𝐴 ) = suc ∩ ( rank “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		scott0b	⊢ ( 𝐴 = ∅ ↔ Scott 𝐴 = ∅ )
2	1	necon3bii	⊢ ( 𝐴 ≠ ∅ ↔ Scott 𝐴 ≠ ∅ )
3		n0	⊢ ( Scott 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ Scott 𝐴 )
4	2 3	sylbb	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 𝑥 ∈ Scott 𝐴 )
5		id	⊢ ( 𝑥 ∈ Scott 𝐴 → 𝑥 ∈ Scott 𝐴 )
6	5	scottrankd	⊢ ( 𝑥 ∈ Scott 𝐴 → ( rank ‘ Scott 𝐴 ) = suc ( rank ‘ 𝑥 ) )
7		elscottrank	⊢ ( 𝑥 ∈ Scott 𝐴 → ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐴 ) )
8	7	suceqd	⊢ ( 𝑥 ∈ Scott 𝐴 → suc ( rank ‘ 𝑥 ) = suc ∩ ( rank “ 𝐴 ) )
9	6 8	eqtrd	⊢ ( 𝑥 ∈ Scott 𝐴 → ( rank ‘ Scott 𝐴 ) = suc ∩ ( rank “ 𝐴 ) )
10	9	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ Scott 𝐴 → ( rank ‘ Scott 𝐴 ) = suc ∩ ( rank “ 𝐴 ) )
11	4 10	syl	⊢ ( 𝐴 ≠ ∅ → ( rank ‘ Scott 𝐴 ) = suc ∩ ( rank “ 𝐴 ) )