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 ⊢ Scott x | φ = x | φ ∧ ∀ y ψ → rank ⁡ x ⊆ rank ⁡ y

Proof

Step Hyp Ref Expression
1 scottabf.1 ⊢ Ⅎ x ψ
2 scottabf.2 ⊢ x = y → φ ↔ ψ
3 df-scott ⊢ Scott x | φ = 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 ↔ ∀ z z ∈ x | φ ∧ ∀ w ∈ x | φ rank ⁡ z ⊆ rank ⁡ w ↔ z ∈ x | φ ∧ ∀ y ψ → rank ⁡ x ⊆ rank ⁡ y
6 nfsab1 ⊢ Ⅎ x z ∈ x | φ
7 nfab1 ⊢ Ⅎ _ x x | φ
8 nfv ⊢ Ⅎ x rank ⁡ z ⊆ rank ⁡ w
9 7 8 nfralw ⊢ Ⅎ x ∀ w ∈ x | φ rank ⁡ z ⊆ rank ⁡ w
10 6 9 nfan ⊢ Ⅎ x z ∈ 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 | φ ↔ y x φ
16 1 2 sbiev ⊢ y x φ ↔ ψ
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 ↔ ∀ w w ∈ x | φ → rank ⁡ z ⊆ rank ⁡ w
28 df-ral ⊢ ∀ w ∈ x | φ rank ⁡ z ⊆ rank ⁡ w ↔ ∀ w w ∈ 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 ⊢ Scott x | φ = x | φ ∧ ∀ y ψ → rank ⁡ x ⊆ rank ⁡ y