Metamath Proof Explorer

Theorem scottrankd

Description: Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

Ref Expression
Hypothesis scottrankd.1 ⊢ φ → B ∈ Scott A
Assertion scottrankd ⊢ φ → rank ⁡ Scott A = suc ⁡ rank ⁡ B

Proof

Step Hyp Ref Expression
1 scottrankd.1 ⊢ φ → B ∈ Scott A
2 scottex2 ⊢ Scott A ∈ V
3 2 rankval4 ⊢ rank ⁡ Scott A = ⋃ x ∈ Scott A suc ⁡ rank ⁡ x
4 3 a1i ⊢ φ → rank ⁡ Scott A = ⋃ x ∈ Scott A suc ⁡ rank ⁡ x
5 1 adantr ⊢ φ ∧ x ∈ Scott A → B ∈ Scott A
6 simpr ⊢ φ ∧ x ∈ Scott A → x ∈ Scott A
7 5 6 scottelrankd ⊢ φ ∧ x ∈ Scott A → rank ⁡ B ⊆ rank ⁡ x
8 6 5 scottelrankd ⊢ φ ∧ x ∈ Scott A → rank ⁡ x ⊆ rank ⁡ B
9 7 8 eqssd ⊢ φ ∧ x ∈ Scott A → rank ⁡ B = rank ⁡ x
10 9 suceqd ⊢ φ ∧ x ∈ Scott A → suc ⁡ rank ⁡ B = suc ⁡ rank ⁡ x
11 10 iuneq2dv ⊢ φ → ⋃ x ∈ Scott A suc ⁡ rank ⁡ B = ⋃ x ∈ Scott A suc ⁡ rank ⁡ x
12 1 ne0d ⊢ φ → Scott A ≠ ∅
13 iunconst ⊢ Scott A ≠ ∅ → ⋃ x ∈ Scott A suc ⁡ rank ⁡ B = suc ⁡ rank ⁡ B
14 12 13 syl ⊢ φ → ⋃ x ∈ Scott A suc ⁡ rank ⁡ B = suc ⁡ rank ⁡ B
15 4 11 14 3eqtr2d ⊢ φ → rank ⁡ Scott A = suc ⁡ rank ⁡ B