Metamath Proof Explorer

Theorem scott0f

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

Ref Expression
Hypotheses scott0f.1 ⊢ Ⅎ _ y A
scott0f.2 ⊢ Ⅎ _ x A
Assertion scott0f ⊢ A = ∅ ↔ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = ∅

Proof

Step Hyp Ref Expression
1 scott0f.1 ⊢ Ⅎ _ y A
2 scott0f.2 ⊢ Ⅎ _ x A
3 scott0 ⊢ A = ∅ ↔ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = ∅
4 nfcv ⊢ Ⅎ _ z A
5 nfv ⊢ Ⅎ z rank ⁡ x ⊆ rank ⁡ y
6 nfv ⊢ Ⅎ y rank ⁡ x ⊆ rank ⁡ z
7 fveq2 ⊢ y = z → rank ⁡ y = rank ⁡ z
8 7 sseq2d ⊢ y = z → rank ⁡ x ⊆ rank ⁡ y ↔ rank ⁡ x ⊆ rank ⁡ z
9 1 4 5 6 8 cbvralfw ⊢ ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
10 9 rabbii ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
11 nfcv ⊢ Ⅎ _ w A
12 nfv ⊢ Ⅎ x rank ⁡ w ⊆ rank ⁡ z
13 2 12 nfralw ⊢ Ⅎ x ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
14 nfv ⊢ Ⅎ w ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
15 fveq2 ⊢ w = x → rank ⁡ w = rank ⁡ x
16 15 sseq1d ⊢ w = x → rank ⁡ w ⊆ rank ⁡ z ↔ rank ⁡ x ⊆ rank ⁡ z
17 16 ralbidv ⊢ w = x → ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
18 11 2 13 14 17 cbvrabw ⊢ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
19 10 18 eqtr4i ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
20 19 eqeq1i ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = ∅ ↔ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = ∅
21 3 20 bitr4i ⊢ A = ∅ ↔ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = ∅