Metamath Proof Explorer

Theorem scottexf

Description: A version of scottex with nonfree variables instead of distinct variables. (Contributed by Giovanni Mascellani, 19-Aug-2018)

Ref Expression
Hypotheses scottexf.1 ⊢ Ⅎ _ y A
scottexf.2 ⊢ Ⅎ _ x A
Assertion scottexf ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ∈ V

Proof

Step Hyp Ref Expression
1 scottexf.1 ⊢ Ⅎ _ y A
2 scottexf.2 ⊢ Ⅎ _ x A
3 nfcv ⊢ Ⅎ _ z A
4 nfv ⊢ Ⅎ z rank ⁡ x ⊆ rank ⁡ y
5 nfv ⊢ Ⅎ y rank ⁡ x ⊆ rank ⁡ z
6 fveq2 ⊢ y = z → rank ⁡ y = rank ⁡ z
7 6 sseq2d ⊢ y = z → rank ⁡ x ⊆ rank ⁡ y ↔ rank ⁡ x ⊆ rank ⁡ z
8 1 3 4 5 7 cbvralfw ⊢ ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
9 8 rabbii ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
10 nfcv ⊢ Ⅎ _ w A
11 nfv ⊢ Ⅎ x rank ⁡ w ⊆ rank ⁡ z
12 2 11 nfralw ⊢ Ⅎ x ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
13 nfv ⊢ Ⅎ w ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
14 fveq2 ⊢ w = x → rank ⁡ w = rank ⁡ x
15 14 sseq1d ⊢ w = x → rank ⁡ w ⊆ rank ⁡ z ↔ rank ⁡ x ⊆ rank ⁡ z
16 15 ralbidv ⊢ w = x → ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
17 10 2 12 13 16 cbvrabw ⊢ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
18 9 17 eqtr4i ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
19 df-scott ⊢ Scott A = w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
20 scottex ⊢ Scott A ∈ V
21 19 20 eqeltrri ⊢ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z ∈ V
22 18 21 eqeltri ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ∈ V