Metamath Proof Explorer

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 ∈ B → rank ⁡ Scott B ⊆ suc ⁡ rank ⁡ A

Proof

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