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	|- ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) )

Proof

Step	Hyp	Ref	Expression
1		id	|- ( x e. Scott B -> x e. Scott B )
2	1	scottrankd	|- ( x e. Scott B -> ( rank ` Scott B ) = suc ( rank ` x ) )
3	2	adantr	|- ( ( x e. Scott B /\ A e. B ) -> ( rank ` Scott B ) = suc ( rank ` x ) )
4		elscottrankss	|- ( ( x e. Scott B /\ A e. B ) -> ( rank ` x ) C_ ( rank ` A ) )
5		rankon	|- ( rank ` x ) e. On
6	5	onordi	|- Ord ( rank ` x )
7		rankon	|- ( rank ` A ) e. On
8	7	onordi	|- Ord ( rank ` A )
9		ordsucsssuc	|- ( ( Ord ( rank ` x ) /\ Ord ( rank ` A ) ) -> ( ( rank ` x ) C_ ( rank ` A ) <-> suc ( rank ` x ) C_ suc ( rank ` A ) ) )
10	6 8 9	mp2an	|- ( ( rank ` x ) C_ ( rank ` A ) <-> suc ( rank ` x ) C_ suc ( rank ` A ) )
11	4 10	sylib	|- ( ( x e. Scott B /\ A e. B ) -> suc ( rank ` x ) C_ suc ( rank ` A ) )
12	3 11	eqsstrd	|- ( ( x e. Scott B /\ A e. B ) -> ( rank ` Scott B ) C_ suc ( rank ` A ) )
13	12	ex	|- ( x e. Scott B -> ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) ) )
14	13	exlimiv	|- ( E. x x e. Scott B -> ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) ) )
15		neq0	|- ( -. Scott B = (/) <-> E. x x e. Scott B )
16	15	con1bii	|- ( -. E. x x e. Scott B <-> Scott B = (/) )
17		scottex2	|- Scott B e. _V
18	17	rankeq0	|- ( Scott B = (/) <-> ( rank ` Scott B ) = (/) )
19		0ss	|- (/) C_ suc ( rank ` A )
20		sseq1	|- ( ( rank ` Scott B ) = (/) -> ( ( rank ` Scott B ) C_ suc ( rank ` A ) <-> (/) C_ suc ( rank ` A ) ) )
21	19 20	mpbiri	|- ( ( rank ` Scott B ) = (/) -> ( rank ` Scott B ) C_ suc ( rank ` A ) )
22	18 21	sylbi	|- ( Scott B = (/) -> ( rank ` Scott B ) C_ suc ( rank ` A ) )
23	16 22	sylbi	|- ( -. E. x x e. Scott B -> ( rank ` Scott B ) C_ suc ( rank ` A ) )
24	23	a1d	|- ( -. E. x x e. Scott B -> ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) ) )
25	14 24	pm2.61i	|- ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) )