Proof of Theorem rabrsndc
Step | Hyp | Ref
| Expression |
1 | | rabrsndc.1 |
. . . . . 6
⊢ A ∈
V |
2 | | rabrsndc.2 |
. . . . . . . 8
⊢
DECID φ |
3 | | pm2.1dc 744 |
. . . . . . . 8
⊢
(DECID φ →
(¬ φ
∨ φ)) |
4 | 2, 3 | ax-mp 7 |
. . . . . . 7
⊢ (¬
φ ∨
φ) |
5 | 4 | sbcth 2771 |
. . . . . 6
⊢ (A ∈ V →
[A / x](¬ φ ∨ φ)) |
6 | 1, 5 | ax-mp 7 |
. . . . 5
⊢
[A / x](¬ φ ∨ φ) |
7 | | sbcor 2801 |
. . . . 5
⊢
([A / x](¬ φ ∨ φ) ↔ ([A / x]
¬ φ
∨ [A / x]φ)) |
8 | 6, 7 | mpbi 133 |
. . . 4
⊢
([A / x] ¬ φ ∨
[A / x]φ) |
9 | | ralsns 3399 |
. . . . . 6
⊢ (A ∈ V →
(∀x
∈ {A}
¬ φ ↔ [A / x]
¬ φ)) |
10 | 1, 9 | ax-mp 7 |
. . . . 5
⊢ (∀x ∈ {A} ¬
φ ↔ [A / x]
¬ φ) |
11 | | ralsns 3399 |
. . . . . 6
⊢ (A ∈ V →
(∀x
∈ {A}φ ↔
[A / x]φ)) |
12 | 1, 11 | ax-mp 7 |
. . . . 5
⊢ (∀x ∈ {A}φ ↔ [A / x]φ) |
13 | 10, 12 | orbi12i 680 |
. . . 4
⊢ ((∀x ∈ {A} ¬
φ ∨
∀x
∈ {A}φ) ↔
([A / x] ¬ φ ∨
[A / x]φ)) |
14 | 8, 13 | mpbir 134 |
. . 3
⊢ (∀x ∈ {A} ¬
φ ∨
∀x
∈ {A}φ) |
15 | | rabeq0 3241 |
. . . 4
⊢
({x ∈ {A} ∣
φ} = ∅ ↔ ∀x ∈ {A} ¬
φ) |
16 | | eqcom 2039 |
. . . . 5
⊢
({x ∈ {A} ∣
φ} = {A} ↔ {A} =
{x ∈
{A} ∣ φ}) |
17 | | rabid2 2480 |
. . . . 5
⊢
({A} = {x ∈ {A} ∣ φ} ↔ ∀x ∈ {A}φ) |
18 | 16, 17 | bitri 173 |
. . . 4
⊢
({x ∈ {A} ∣
φ} = {A} ↔ ∀x ∈ {A}φ) |
19 | 15, 18 | orbi12i 680 |
. . 3
⊢
(({x ∈ {A} ∣
φ} = ∅
∨ {x ∈ {A} ∣
φ} = {A}) ↔ (∀x ∈ {A} ¬
φ ∨
∀x
∈ {A}φ)) |
20 | 14, 19 | mpbir 134 |
. 2
⊢
({x ∈ {A} ∣
φ} = ∅
∨ {x ∈ {A} ∣
φ} = {A}) |
21 | | eqeq1 2043 |
. . 3
⊢ (𝑀 = {x ∈ {A} ∣ φ} → (𝑀 = ∅ ↔ {x ∈ {A} ∣ φ} = ∅)) |
22 | | eqeq1 2043 |
. . 3
⊢ (𝑀 = {x ∈ {A} ∣ φ} → (𝑀 = {A}
↔ {x ∈ {A} ∣
φ} = {A})) |
23 | 21, 22 | orbi12d 706 |
. 2
⊢ (𝑀 = {x ∈ {A} ∣ φ} → ((𝑀 = ∅
∨ 𝑀 = {A}) ↔ ({x
∈ {A}
∣ φ} = ∅ ∨ {x ∈ {A} ∣
φ} = {A}))) |
24 | 20, 23 | mpbiri 157 |
1
⊢ (𝑀 = {x ∈ {A} ∣ φ} → (𝑀 = ∅
∨ 𝑀 = {A})) |