Theorem rankscottu

Description: An upper bound on the rank of a Scott's trick set. (Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	rankscottu	⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 ∈ Scott 𝐵 → 𝑥 ∈ Scott 𝐵 )
2	1	scottrankd	⊢ ( 𝑥 ∈ Scott 𝐵 → ( rank ‘ Scott 𝐵 ) = suc ( rank ‘ 𝑥 ) )
3	2	adantr	⊢ ( ( 𝑥 ∈ Scott 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ Scott 𝐵 ) = suc ( rank ‘ 𝑥 ) )
4		elscottrankss	⊢ ( ( 𝑥 ∈ Scott 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
5		rankon	⊢ ( rank ‘ 𝑥 ) ∈ On
6	5	onordi	⊢ Ord ( rank ‘ 𝑥 )
7		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
8	7	onordi	⊢ Ord ( rank ‘ 𝐴 )
9		ordsucsssuc	⊢ ( ( Ord ( rank ‘ 𝑥 ) ∧ Ord ( rank ‘ 𝐴 ) ) → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) ↔ suc ( rank ‘ 𝑥 ) ⊆ suc ( rank ‘ 𝐴 ) ) )
10	6 8 9	mp2an	⊢ ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) ↔ suc ( rank ‘ 𝑥 ) ⊆ suc ( rank ‘ 𝐴 ) )
11	4 10	sylib	⊢ ( ( 𝑥 ∈ Scott 𝐵 ∧ 𝐴 ∈ 𝐵 ) → suc ( rank ‘ 𝑥 ) ⊆ suc ( rank ‘ 𝐴 ) )
12	3 11	eqsstrd	⊢ ( ( 𝑥 ∈ Scott 𝐵 ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )
13	12	ex	⊢ ( 𝑥 ∈ Scott 𝐵 → ( 𝐴 ∈ 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) ) )
14	13	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ Scott 𝐵 → ( 𝐴 ∈ 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) ) )
15		neq0	⊢ ( ¬ Scott 𝐵 = ∅ ↔ ∃ 𝑥 𝑥 ∈ Scott 𝐵 )
16	15	con1bii	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ Scott 𝐵 ↔ Scott 𝐵 = ∅ )
17		scottex	⊢ Scott 𝐵 ∈ V
18	17	rankeq0	⊢ ( Scott 𝐵 = ∅ ↔ ( rank ‘ Scott 𝐵 ) = ∅ )
19		0ss	⊢ ∅ ⊆ suc ( rank ‘ 𝐴 )
20		sseq1	⊢ ( ( rank ‘ Scott 𝐵 ) = ∅ → ( ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) ↔ ∅ ⊆ suc ( rank ‘ 𝐴 ) ) )
21	19 20	mpbiri	⊢ ( ( rank ‘ Scott 𝐵 ) = ∅ → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )
22	18 21	sylbi	⊢ ( Scott 𝐵 = ∅ → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )
23	16 22	sylbi	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ Scott 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )
24	23	a1d	⊢ ( ¬ ∃ 𝑥 𝑥 ∈ Scott 𝐵 → ( 𝐴 ∈ 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) ) )
25	14 24	pm2.61i	⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ Scott 𝐵 ) ⊆ suc ( rank ‘ 𝐴 ) )