Step | Hyp | Ref
| Expression |
1 | | onsucelsucexmidlem 4513 |
. . . 4
⊢ {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)} ∈
On |
2 | | pp0ex 4175 |
. . . . 5
⊢ {∅,
{∅}} ∈ V |
3 | 2 | rabex 4133 |
. . . 4
⊢ {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = {∅} ∨
𝜑)} ∈ V |
4 | | prexg 4196 |
. . . 4
⊢ (({𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)} ∈ On ∧ {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = {∅} ∨
𝜑)} ∈ V) → {{𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} ∈ V) |
5 | 1, 3, 4 | mp2an 424 |
. . 3
⊢ {{𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} ∈ V |
6 | | raleq 2665 |
. . . 4
⊢ (𝑥 = {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} → (∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∀𝑧 ∈ {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}}∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))) |
7 | 6 | exbidv 1818 |
. . 3
⊢ (𝑥 = {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} → (∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃𝑦∀𝑧 ∈ {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}}∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))) |
8 | | acexmidlemv.choice |
. . 3
⊢
∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) |
9 | 5, 7, 8 | vtocl 2784 |
. 2
⊢
∃𝑦∀𝑧 ∈ {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}}∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) |
10 | | eqeq1 2177 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (𝑠 = ∅ ↔ 𝑡 = ∅)) |
11 | 10 | orbi1d 786 |
. . . . 5
⊢ (𝑠 = 𝑡 → ((𝑠 = ∅ ∨ 𝜑) ↔ (𝑡 = ∅ ∨ 𝜑))) |
12 | 11 | cbvrabv 2729 |
. . . 4
⊢ {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)} = {𝑡 ∈ {∅, {∅}} ∣ (𝑡 = ∅ ∨ 𝜑)} |
13 | | eqeq1 2177 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (𝑠 = {∅} ↔ 𝑡 = {∅})) |
14 | 13 | orbi1d 786 |
. . . . 5
⊢ (𝑠 = 𝑡 → ((𝑠 = {∅} ∨ 𝜑) ↔ (𝑡 = {∅} ∨ 𝜑))) |
15 | 14 | cbvrabv 2729 |
. . . 4
⊢ {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = {∅} ∨
𝜑)} = {𝑡 ∈ {∅, {∅}} ∣ (𝑡 = {∅} ∨ 𝜑)} |
16 | | eqid 2170 |
. . . 4
⊢ {{𝑠 ∈ {∅, {∅}}
∣ (𝑠 = ∅ ∨
𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} = {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}} |
17 | 12, 15, 16 | acexmidlem2 5850 |
. . 3
⊢
(∀𝑧 ∈
{{𝑠 ∈ {∅,
{∅}} ∣ (𝑠 =
∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}}
∣ (𝑠 = {∅} ∨
𝜑)}}∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑)) |
18 | 17 | exlimiv 1591 |
. 2
⊢
(∃𝑦∀𝑧 ∈ {{𝑠 ∈ {∅, {∅}} ∣ (𝑠 = ∅ ∨ 𝜑)}, {𝑠 ∈ {∅, {∅}} ∣ (𝑠 = {∅} ∨ 𝜑)}}∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) → (𝜑 ∨ ¬ 𝜑)) |
19 | 9, 18 | ax-mp 5 |
1
⊢ (𝜑 ∨ ¬ 𝜑) |