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∈ScottA
scottelrankd.2 ⊢φ→C∈ScottA
Assertion scottelrankd ⊢φ→rank⁡B⊆rank⁡C

Proof

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