Metamath Proof Explorer

Theorem scottabf

Description: Value of the Scott operation at a class abstraction. Variant of scottab with a nonfreeness hypothesis instead of a disjoint variable condition. (Contributed by Rohan Ridenour, 14-Aug-2023)

Ref Expression
Hypotheses scottabf.1 ⊢Ⅎxψ
scottabf.2 ⊢x=y→φ↔ψ
Assertion scottabf ⊢Scottx|φ=x|φ∧∀yψ→rank⁡x⊆rank⁡y

Proof

Step Hyp Ref Expression
1 scottabf.1 ⊢Ⅎxψ
2 scottabf.2 ⊢x=y→φ↔ψ
3 df-scott ⊢Scottx|φ=z∈x|φ|∀w∈x|φrank⁡z⊆rank⁡w
4 df-rab ⊢z∈x|φ|∀w∈x|φrank⁡z⊆rank⁡w=z|z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w
5 eqabcb ⊢z|z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w=x|φ∧∀yψ→rank⁡x⊆rank⁡y↔∀zz∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w↔z∈x|φ∧∀yψ→rank⁡x⊆rank⁡y
6 nfsab1 ⊢Ⅎxz∈x|φ
7 nfab1 ⊢Ⅎ_xx|φ
8 nfv ⊢Ⅎxrank⁡z⊆rank⁡w
9 7 8 nfralw ⊢Ⅎx∀w∈x|φrank⁡z⊆rank⁡w
10 6 9 nfan ⊢Ⅎxz∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w
11 vex ⊢z∈V
12 abid ⊢x∈x|φ↔φ
13 eleq1w ⊢x=z→x∈x|φ↔z∈x|φ
14 12 13 bitr3id ⊢x=z→φ↔z∈x|φ
15 df-clab ⊢y∈x|φ↔yxφ
16 1 2 sbiev ⊢yxφ↔ψ
17 15 16 bitr2i ⊢ψ↔y∈x|φ
18 eleq1w ⊢y=w→y∈x|φ↔w∈x|φ
19 17 18 bitrid ⊢y=w→ψ↔w∈x|φ
20 19 adantl ⊢x=z∧y=w→ψ↔w∈x|φ
21 simpl ⊢x=z∧y=w→x=z
22 21 fveq2d ⊢x=z∧y=w→rank⁡x=rank⁡z
23 simpr ⊢x=z∧y=w→y=w
24 23 fveq2d ⊢x=z∧y=w→rank⁡y=rank⁡w
25 22 24 sseq12d ⊢x=z∧y=w→rank⁡x⊆rank⁡y↔rank⁡z⊆rank⁡w
26 20 25 imbi12d ⊢x=z∧y=w→ψ→rank⁡x⊆rank⁡y↔w∈x|φ→rank⁡z⊆rank⁡w
27 26 cbvaldvaw ⊢x=z→∀yψ→rank⁡x⊆rank⁡y↔∀ww∈x|φ→rank⁡z⊆rank⁡w
28 df-ral ⊢∀w∈x|φrank⁡z⊆rank⁡w↔∀ww∈x|φ→rank⁡z⊆rank⁡w
29 27 28 bitr4di ⊢x=z→∀yψ→rank⁡x⊆rank⁡y↔∀w∈x|φrank⁡z⊆rank⁡w
30 14 29 anbi12d ⊢x=z→φ∧∀yψ→rank⁡x⊆rank⁡y↔z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w
31 10 11 30 elabf ⊢z∈x|φ∧∀yψ→rank⁡x⊆rank⁡y↔z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w
32 31 bicomi ⊢z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w↔z∈x|φ∧∀yψ→rank⁡x⊆rank⁡y
33 5 32 mpgbir ⊢z|z∈x|φ∧∀w∈x|φrank⁡z⊆rank⁡w=x|φ∧∀yψ→rank⁡x⊆rank⁡y
34 3 4 33 3eqtri ⊢Scottx|φ=x|φ∧∀yψ→rank⁡x⊆rank⁡y