Proof of Theorem regexmidlem1
Step | Hyp | Ref
| Expression |
1 | | eqeq1 2172 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 = {∅} ↔ 𝑦 = {∅})) |
2 | | eqeq1 2172 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
3 | 2 | anbi1d 461 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → ((𝑥 = ∅ ∧ 𝜑) ↔ (𝑦 = ∅ ∧ 𝜑))) |
4 | 1, 3 | orbi12d 783 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑥 = {∅} ∨ (𝑥 = ∅ ∧ 𝜑)) ↔ (𝑦 = {∅} ∨ (𝑦 = ∅ ∧ 𝜑)))) |
5 | | regexmidlemm.a |
. . . . . 6
⊢ 𝐴 = {𝑥 ∈ {∅, {∅}} ∣ (𝑥 = {∅} ∨ (𝑥 = ∅ ∧ 𝜑))} |
6 | 4, 5 | elrab2 2885 |
. . . . 5
⊢ (𝑦 ∈ 𝐴 ↔ (𝑦 ∈ {∅, {∅}} ∧ (𝑦 = {∅} ∨ (𝑦 = ∅ ∧ 𝜑)))) |
7 | 6 | simprbi 273 |
. . . 4
⊢ (𝑦 ∈ 𝐴 → (𝑦 = {∅} ∨ (𝑦 = ∅ ∧ 𝜑))) |
8 | | 0ex 4109 |
. . . . . . . . 9
⊢ ∅
∈ V |
9 | 8 | snid 3607 |
. . . . . . . 8
⊢ ∅
∈ {∅} |
10 | | eleq2 2230 |
. . . . . . . 8
⊢ (𝑦 = {∅} → (∅
∈ 𝑦 ↔ ∅
∈ {∅})) |
11 | 9, 10 | mpbiri 167 |
. . . . . . 7
⊢ (𝑦 = {∅} → ∅
∈ 𝑦) |
12 | | eleq1 2229 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → (𝑧 ∈ 𝑦 ↔ ∅ ∈ 𝑦)) |
13 | | eleq1 2229 |
. . . . . . . . . 10
⊢ (𝑧 = ∅ → (𝑧 ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
14 | 13 | notbid 657 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → (¬ 𝑧 ∈ 𝐴 ↔ ¬ ∅ ∈ 𝐴)) |
15 | 12, 14 | imbi12d 233 |
. . . . . . . 8
⊢ (𝑧 = ∅ → ((𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) ↔ (∅ ∈ 𝑦 → ¬ ∅ ∈ 𝐴))) |
16 | 8, 15 | spcv 2820 |
. . . . . . 7
⊢
(∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → (∅ ∈ 𝑦 → ¬ ∅ ∈ 𝐴)) |
17 | 11, 16 | syl5com 29 |
. . . . . 6
⊢ (𝑦 = {∅} →
(∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → ¬ ∅ ∈ 𝐴)) |
18 | 8 | prid1 3682 |
. . . . . . . . . 10
⊢ ∅
∈ {∅, {∅}} |
19 | | eqeq1 2172 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑥 = {∅} ↔ ∅ =
{∅})) |
20 | | eqeq1 2172 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 = ∅ ↔ ∅ =
∅)) |
21 | 20 | anbi1d 461 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ((𝑥 = ∅ ∧ 𝜑) ↔ (∅ = ∅ ∧ 𝜑))) |
22 | 19, 21 | orbi12d 783 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ((𝑥 = {∅} ∨ (𝑥 = ∅ ∧ 𝜑)) ↔ (∅ = {∅} ∨ (∅
= ∅ ∧ 𝜑)))) |
23 | 22, 5 | elrab2 2885 |
. . . . . . . . . 10
⊢ (∅
∈ 𝐴 ↔ (∅
∈ {∅, {∅}} ∧ (∅ = {∅} ∨ (∅ = ∅
∧ 𝜑)))) |
24 | 18, 23 | mpbiran 930 |
. . . . . . . . 9
⊢ (∅
∈ 𝐴 ↔ (∅ =
{∅} ∨ (∅ = ∅ ∧ 𝜑))) |
25 | | pm2.46 729 |
. . . . . . . . 9
⊢ (¬
(∅ = {∅} ∨ (∅ = ∅ ∧ 𝜑)) → ¬ (∅ = ∅ ∧
𝜑)) |
26 | 24, 25 | sylnbi 668 |
. . . . . . . 8
⊢ (¬
∅ ∈ 𝐴 →
¬ (∅ = ∅ ∧ 𝜑)) |
27 | | eqid 2165 |
. . . . . . . . 9
⊢ ∅ =
∅ |
28 | 27 | biantrur 301 |
. . . . . . . 8
⊢ (𝜑 ↔ (∅ = ∅ ∧
𝜑)) |
29 | 26, 28 | sylnibr 667 |
. . . . . . 7
⊢ (¬
∅ ∈ 𝐴 →
¬ 𝜑) |
30 | 29 | olcd 724 |
. . . . . 6
⊢ (¬
∅ ∈ 𝐴 →
(𝜑 ∨ ¬ 𝜑)) |
31 | 17, 30 | syl6 33 |
. . . . 5
⊢ (𝑦 = {∅} →
(∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → (𝜑 ∨ ¬ 𝜑))) |
32 | | orc 702 |
. . . . . . 7
⊢ (𝜑 → (𝜑 ∨ ¬ 𝜑)) |
33 | 32 | adantl 275 |
. . . . . 6
⊢ ((𝑦 = ∅ ∧ 𝜑) → (𝜑 ∨ ¬ 𝜑)) |
34 | 33 | a1d 22 |
. . . . 5
⊢ ((𝑦 = ∅ ∧ 𝜑) → (∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → (𝜑 ∨ ¬ 𝜑))) |
35 | 31, 34 | jaoi 706 |
. . . 4
⊢ ((𝑦 = {∅} ∨ (𝑦 = ∅ ∧ 𝜑)) → (∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → (𝜑 ∨ ¬ 𝜑))) |
36 | 7, 35 | syl 14 |
. . 3
⊢ (𝑦 ∈ 𝐴 → (∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴) → (𝜑 ∨ ¬ 𝜑))) |
37 | 36 | imp 123 |
. 2
⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴)) → (𝜑 ∨ ¬ 𝜑)) |
38 | 37 | exlimiv 1586 |
1
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝐴)) → (𝜑 ∨ ¬ 𝜑)) |