Metamath Proof Explorer

Theorem scott0f

Description: A version of scott0b 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 df-scott ⊢ Scott A = w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
4 3 eqeq1i ⊢ Scott A = ∅ ↔ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = ∅
5 scott0b ⊢ A = ∅ ↔ Scott A = ∅
6 nfcv ⊢ Ⅎ _ z A
7 nfv ⊢ Ⅎ z rank ⁡ x ⊆ rank ⁡ y
8 nfv ⊢ Ⅎ y rank ⁡ x ⊆ rank ⁡ z
9 fveq2 ⊢ y = z → rank ⁡ y = rank ⁡ z
10 9 sseq2d ⊢ y = z → rank ⁡ x ⊆ rank ⁡ y ↔ rank ⁡ x ⊆ rank ⁡ z
11 1 6 7 8 10 cbvralfw ⊢ ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
12 11 rabbii ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
13 nfcv ⊢ Ⅎ _ w A
14 nfv ⊢ Ⅎ x rank ⁡ w ⊆ rank ⁡ z
15 2 14 nfralw ⊢ Ⅎ x ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
16 nfv ⊢ Ⅎ w ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
17 fveq2 ⊢ w = x → rank ⁡ w = rank ⁡ x
18 17 sseq1d ⊢ w = x → rank ⁡ w ⊆ rank ⁡ z ↔ rank ⁡ x ⊆ rank ⁡ z
19 18 ralbidv ⊢ w = x → ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z ↔ ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
20 13 2 15 16 19 cbvrabw ⊢ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = x ∈ A | ∀ z ∈ A rank ⁡ x ⊆ rank ⁡ z
21 12 20 eqtr4i ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z
22 21 eqeq1i ⊢ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = ∅ ↔ w ∈ A | ∀ z ∈ A rank ⁡ w ⊆ rank ⁡ z = ∅
23 4 5 22 3bitr4i ⊢ A = ∅ ↔ x ∈ A | ∀ y ∈ A rank ⁡ x ⊆ rank ⁡ y = ∅