Metamath Proof Explorer

Theorem scottelrankd

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

Ref Expression
Hypotheses scottelrankd.1 ⊢ φ → B ∈ Scott A
scottelrankd.2 ⊢ φ → C ∈ Scott A
Assertion scottelrankd ⊢ φ → rank ⁡ B ⊆ rank ⁡ C

Proof

Step Hyp Ref Expression
1 scottelrankd.1 ⊢ φ → B ∈ Scott A
2 scottelrankd.2 ⊢ φ → C ∈ Scott A
3 fveq2 ⊢ y = C → rank ⁡ y = rank ⁡ C
4 3 sseq2d ⊢ y = C → rank ⁡ B ⊆ rank ⁡ y ↔ rank ⁡ B ⊆ rank ⁡ C
5 df-scott ⊢ Scott A = x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y
6 1 5 eleqtrdi ⊢ φ → B ∈ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y
7 fveq2 ⊢ x = B → rank ⁡ x = rank ⁡ B
8 7 sseq1d ⊢ x = B → rank ⁡ x ⊆ rank ⁡ y ↔ rank ⁡ B ⊆ rank ⁡ y
9 8 ralbidv ⊢ x = B → ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ y ∈ A rank ⁡ B ⊆ rank ⁡ y
10 9 elrab ⊢ B ∈ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ↔ B ∈ A ∧ ∀ y ∈ A rank ⁡ B ⊆ rank ⁡ y
11 6 10 sylib ⊢ φ → B ∈ A ∧ ∀ y ∈ A rank ⁡ B ⊆ rank ⁡ y
12 11 simprd ⊢ φ → ∀ y ∈ A rank ⁡ B ⊆ rank ⁡ y
13 2 5 eleqtrdi ⊢ φ → C ∈ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y
14 elrabi ⊢ C ∈ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y → C ∈ A
15 13 14 syl ⊢ φ → C ∈ A
16 4 12 15 rspcdva ⊢ φ → rank ⁡ B ⊆ rank ⁡ C