Step | Hyp | Ref
| Expression |
1 | | 2oneel 7255 |
. . . 4
⊢
⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} |
2 | | 2omotaplemap 7256 |
. . . . . 6
⊢ (¬
¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o) |
3 | 2 | adantl 277 |
. . . . 5
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o) |
4 | | 2onn 6522 |
. . . . . . . . . 10
⊢
2o ∈ ω |
5 | 4 | elexi 2750 |
. . . . . . . . 9
⊢
2o ∈ V |
6 | 5, 5 | xpex 4742 |
. . . . . . . 8
⊢
(2o × 2o) ∈ V |
7 | | opabssxp 4701 |
. . . . . . . 8
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} ⊆ (2o
× 2o) |
8 | 6, 7 | ssexi 4142 |
. . . . . . 7
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} ∈ V |
9 | 8 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} ∈ V) |
10 | | opabssxp 4701 |
. . . . . . . 8
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} ⊆ (2o ×
2o) |
11 | 6, 10 | ssexi 4142 |
. . . . . . 7
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} ∈ V |
12 | 11 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ∈ V) |
13 | | simpl 109 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → ∃*𝑟 𝑟 TAp 2o) |
14 | | 2onetap 7254 |
. . . . . . 7
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} TAp
2o |
15 | 14 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} TAp 2o) |
16 | | tapeq1 7251 |
. . . . . . 7
⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} → (𝑟 TAp 2o ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} TAp 2o)) |
17 | | tapeq1 7251 |
. . . . . . 7
⊢ (𝑟 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} → (𝑟 TAp 2o ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o)) |
18 | 16, 17 | mob 2920 |
. . . . . 6
⊢
((({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} ∈ V ∧ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ∈ V) ∧ ∃*𝑟 𝑟 TAp 2o ∧ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} TAp 2o) → ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o)) |
19 | 9, 12, 13, 15, 18 | syl211anc 1244 |
. . . . 5
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o)) |
20 | 3, 19 | mpbird 167 |
. . . 4
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
21 | 1, 20 | eleqtrid 2266 |
. . 3
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) →
⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
22 | | 0lt2o 6442 |
. . . 4
⊢ ∅
∈ 2o |
23 | | 1lt2o 6443 |
. . . 4
⊢
1o ∈ 2o |
24 | | neeq1 2360 |
. . . . . 6
⊢ (𝑢 = ∅ → (𝑢 ≠ 𝑣 ↔ ∅ ≠ 𝑣)) |
25 | 24 | anbi2d 464 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝜑 ∧ 𝑢 ≠ 𝑣) ↔ (𝜑 ∧ ∅ ≠ 𝑣))) |
26 | | neeq2 2361 |
. . . . . 6
⊢ (𝑣 = 1o → (∅
≠ 𝑣 ↔ ∅ ≠
1o)) |
27 | 26 | anbi2d 464 |
. . . . 5
⊢ (𝑣 = 1o → ((𝜑 ∧ ∅ ≠ 𝑣) ↔ (𝜑 ∧ ∅ ≠
1o))) |
28 | 25, 27 | opelopab2 4271 |
. . . 4
⊢ ((∅
∈ 2o ∧ 1o ∈ 2o) →
(⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ ∅ ≠
1o))) |
29 | 22, 23, 28 | mp2an 426 |
. . 3
⊢
(⟨∅, 1o⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ ∅ ≠
1o)) |
30 | 21, 29 | sylib 122 |
. 2
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → (𝜑 ∧ ∅ ≠
1o)) |
31 | 30 | simpld 112 |
1
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → 𝜑) |