Step | Hyp | Ref
| Expression |
1 | | 2oneel 7254 |
. . . 4
⊢
〈∅, 1o〉 ∈ {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} |
2 | | 2omotaplemap 7255 |
. . . . . 6
⊢ (¬
¬ 𝜑 → {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o) |
3 | 2 | adantl 277 |
. . . . 5
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o) |
4 | | 2onn 6521 |
. . . . . . . . . 10
⊢
2o ∈ ω |
5 | 4 | elexi 2749 |
. . . . . . . . 9
⊢
2o ∈ V |
6 | 5, 5 | xpex 4741 |
. . . . . . . 8
⊢
(2o × 2o) ∈ V |
7 | | opabssxp 4700 |
. . . . . . . 8
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} ⊆ (2o
× 2o) |
8 | 6, 7 | ssexi 4141 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} ∈ V |
9 | 8 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} ∈ V) |
10 | | opabssxp 4700 |
. . . . . . . 8
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} ⊆ (2o ×
2o) |
11 | 6, 10 | ssexi 4141 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} ∈ V |
12 | 11 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ∈ V) |
13 | | simpl 109 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → ∃*𝑟 𝑟 TAp 2o) |
14 | | 2onetap 7253 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ 𝑢 ≠ 𝑣)} TAp
2o |
15 | 14 | a1i 9 |
. . . . . 6
⊢
((∃*𝑟 𝑟 TAp 2o ∧ ¬
¬ 𝜑) → {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} TAp 2o) |
16 | | tapeq1 7250 |
. . . . . . 7
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} → (𝑟 TAp 2o ↔ {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
𝑢 ≠ 𝑣)} TAp 2o)) |
17 | | tapeq1 7250 |
. . . . . . 7
⊢ (𝑟 = {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} → (𝑟 TAp 2o ↔ {〈𝑢, 𝑣〉 ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o)) |
18 | 16, 17 | mob 2919 |
. . . . . 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 6441 |
. . . 4
⊢ ∅
∈ 2o |
23 | | 1lt2o 6442 |
. . . 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 4270 |
. . . 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 ∧ ¬
¬ 𝜑) → 𝜑) |