Proof of Theorem acexmidlem2
Step | Hyp | Ref
| Expression |
1 | | df-ral 2305 |
. . . . 5
⊢ (∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∀w(w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
2 | | 19.23v 1760 |
. . . . 5
⊢ (∀w(w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) ↔ (∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
3 | 1, 2 | bitr2i 174 |
. . . 4
⊢ ((∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) |
4 | | acexmidlem.c |
. . . . . . . . 9
⊢ 𝐶 = {A, B} |
5 | 4 | eleq2i 2101 |
. . . . . . . 8
⊢ (z ∈ 𝐶 ↔ z ∈ {A, B}) |
6 | | vex 2554 |
. . . . . . . . 9
⊢ z ∈
V |
7 | 6 | elpr 3385 |
. . . . . . . 8
⊢ (z ∈ {A, B} ↔
(z = A
∨ z =
B)) |
8 | 5, 7 | bitri 173 |
. . . . . . 7
⊢ (z ∈ 𝐶 ↔ (z = A ∨ z = B)) |
9 | | onsucelsucexmidlem1 4213 |
. . . . . . . . . . 11
⊢ ∅
∈ {x
∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} |
10 | | acexmidlem.a |
. . . . . . . . . . 11
⊢ A = {x ∈ {∅, {∅}} ∣ (x = ∅ ∨ φ)} |
11 | 9, 10 | eleqtrri 2110 |
. . . . . . . . . 10
⊢ ∅
∈ A |
12 | | elex2 2564 |
. . . . . . . . . 10
⊢ (∅
∈ A
→ ∃w w ∈ A) |
13 | 11, 12 | ax-mp 7 |
. . . . . . . . 9
⊢ ∃w w ∈ A |
14 | | eleq2 2098 |
. . . . . . . . . 10
⊢ (z = A →
(w ∈
z ↔ w ∈ A)) |
15 | 14 | exbidv 1703 |
. . . . . . . . 9
⊢ (z = A →
(∃w
w ∈
z ↔ ∃w w ∈ A)) |
16 | 13, 15 | mpbiri 157 |
. . . . . . . 8
⊢ (z = A →
∃w
w ∈
z) |
17 | | p0ex 3930 |
. . . . . . . . . . . . 13
⊢ {∅}
∈ V |
18 | 17 | prid2 3468 |
. . . . . . . . . . . 12
⊢ {∅}
∈ {∅, {∅}} |
19 | | eqid 2037 |
. . . . . . . . . . . . 13
⊢ {∅}
= {∅} |
20 | 19 | orci 649 |
. . . . . . . . . . . 12
⊢
({∅} = {∅} ∨ φ) |
21 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
⊢ (x = {∅} → (x = {∅} ↔ {∅} =
{∅})) |
22 | 21 | orbi1d 704 |
. . . . . . . . . . . . 13
⊢ (x = {∅} → ((x = {∅} ∨
φ) ↔ ({∅} = {∅} ∨ φ))) |
23 | 22 | elrab 2692 |
. . . . . . . . . . . 12
⊢
({∅} ∈ {x ∈ {∅,
{∅}} ∣ (x = {∅} ∨ φ)} ↔
({∅} ∈ {∅, {∅}} ∧ ({∅} = {∅}
∨ φ))) |
24 | 18, 20, 23 | mpbir2an 848 |
. . . . . . . . . . 11
⊢ {∅}
∈ {x
∈ {∅, {∅}} ∣ (x = {∅} ∨
φ)} |
25 | | acexmidlem.b |
. . . . . . . . . . 11
⊢ B = {x ∈ {∅, {∅}} ∣ (x = {∅} ∨
φ)} |
26 | 24, 25 | eleqtrri 2110 |
. . . . . . . . . 10
⊢ {∅}
∈ B |
27 | | elex2 2564 |
. . . . . . . . . 10
⊢
({∅} ∈ B → ∃w w ∈ B) |
28 | 26, 27 | ax-mp 7 |
. . . . . . . . 9
⊢ ∃w w ∈ B |
29 | | eleq2 2098 |
. . . . . . . . . 10
⊢ (z = B →
(w ∈
z ↔ w ∈ B)) |
30 | 29 | exbidv 1703 |
. . . . . . . . 9
⊢ (z = B →
(∃w
w ∈
z ↔ ∃w w ∈ B)) |
31 | 28, 30 | mpbiri 157 |
. . . . . . . 8
⊢ (z = B →
∃w
w ∈
z) |
32 | 16, 31 | jaoi 635 |
. . . . . . 7
⊢
((z = A ∨ z = B) →
∃w
w ∈
z) |
33 | 8, 32 | sylbi 114 |
. . . . . 6
⊢ (z ∈ 𝐶 → ∃w w ∈ z) |
34 | | pm2.27 35 |
. . . . . 6
⊢ (∃w w ∈ z → ((∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
35 | 33, 34 | syl 14 |
. . . . 5
⊢ (z ∈ 𝐶 → ((∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) |
36 | 35 | imp 115 |
. . . 4
⊢
((z ∈ 𝐶 ∧ (∃w w ∈ z → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) |
37 | 3, 36 | sylan2br 272 |
. . 3
⊢
((z ∈ 𝐶 ∧ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) → ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) |
38 | 37 | ralimiaa 2377 |
. 2
⊢ (∀z ∈ 𝐶 ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → ∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)) |
39 | 10, 25, 4 | acexmidlem1 5451 |
. 2
⊢ (∀z ∈ 𝐶 ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ
∨ ¬ φ)) |
40 | 38, 39 | syl 14 |
1
⊢ (∀z ∈ 𝐶 ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) → (φ
∨ ¬ φ)) |