Step | Hyp | Ref
| Expression |
1 | | opabssxp 4701 |
. . 3
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} ⊆ (2o ×
2o) |
2 | 1 | a1i 9 |
. 2
⊢ (¬
¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ⊆ (2o ×
2o)) |
3 | | df-br 4005 |
. . . . . . . 8
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
4 | | neeq1 2360 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑎 → (𝑢 ≠ 𝑣 ↔ 𝑎 ≠ 𝑣)) |
5 | 4 | anbi2d 464 |
. . . . . . . . 9
⊢ (𝑢 = 𝑎 → ((𝜑 ∧ 𝑢 ≠ 𝑣) ↔ (𝜑 ∧ 𝑎 ≠ 𝑣))) |
6 | | neeq2 2361 |
. . . . . . . . . 10
⊢ (𝑣 = 𝑏 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑏)) |
7 | 6 | anbi2d 464 |
. . . . . . . . 9
⊢ (𝑣 = 𝑏 → ((𝜑 ∧ 𝑎 ≠ 𝑣) ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
8 | 5, 7 | opelopab2 4271 |
. . . . . . . 8
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
9 | 3, 8 | bitrid 192 |
. . . . . . 7
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
10 | | df-br 4005 |
. . . . . . . 8
⊢ (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ↔ ⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
11 | | neeq1 2360 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑏 → (𝑢 ≠ 𝑣 ↔ 𝑏 ≠ 𝑣)) |
12 | 11 | anbi2d 464 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑏 → ((𝜑 ∧ 𝑢 ≠ 𝑣) ↔ (𝜑 ∧ 𝑏 ≠ 𝑣))) |
13 | | neeq2 2361 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑎 → (𝑏 ≠ 𝑣 ↔ 𝑏 ≠ 𝑎)) |
14 | 13 | anbi2d 464 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑎 → ((𝜑 ∧ 𝑏 ≠ 𝑣) ↔ (𝜑 ∧ 𝑏 ≠ 𝑎))) |
15 | 12, 14 | opelopab2 4271 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 2o ∧
𝑎 ∈ 2o)
→ (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑏 ≠ 𝑎))) |
16 | 15 | ancoms 268 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑏 ≠ 𝑎))) |
17 | | necom 2431 |
. . . . . . . . . 10
⊢ (𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏) |
18 | 17 | anbi2i 457 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑏 ≠ 𝑎) ↔ (𝜑 ∧ 𝑎 ≠ 𝑏)) |
19 | 16, 18 | bitrdi 196 |
. . . . . . . 8
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
20 | 10, 19 | bitrid 192 |
. . . . . . 7
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
21 | 9, 20 | bitr4d 191 |
. . . . . 6
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎)) |
22 | 21 | biimpd 144 |
. . . . 5
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎)) |
23 | 22 | rgen2 2563 |
. . . 4
⊢
∀𝑎 ∈
2o ∀𝑏
∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎) |
24 | 23 | a1i 9 |
. . 3
⊢ (¬
¬ 𝜑 → ∀𝑎 ∈ 2o
∀𝑏 ∈
2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎)) |
25 | | neirr 2356 |
. . . . . 6
⊢ ¬
𝑎 ≠ 𝑎 |
26 | 25 | intnan 929 |
. . . . 5
⊢ ¬
(𝜑 ∧ 𝑎 ≠ 𝑎) |
27 | | df-br 4005 |
. . . . . 6
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
28 | | neeq2 2361 |
. . . . . . . . 9
⊢ (𝑣 = 𝑎 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑎)) |
29 | 28 | anbi2d 464 |
. . . . . . . 8
⊢ (𝑣 = 𝑎 → ((𝜑 ∧ 𝑎 ≠ 𝑣) ↔ (𝜑 ∧ 𝑎 ≠ 𝑎))) |
30 | 5, 29 | opelopab2 4271 |
. . . . . . 7
⊢ ((𝑎 ∈ 2o ∧
𝑎 ∈ 2o)
→ (⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑎))) |
31 | 30 | anidms 397 |
. . . . . 6
⊢ (𝑎 ∈ 2o →
(⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑎))) |
32 | 27, 31 | bitrid 192 |
. . . . 5
⊢ (𝑎 ∈ 2o →
(𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ↔ (𝜑 ∧ 𝑎 ≠ 𝑎))) |
33 | 26, 32 | mtbiri 675 |
. . . 4
⊢ (𝑎 ∈ 2o →
¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎) |
34 | 33 | rgen 2530 |
. . 3
⊢
∀𝑎 ∈
2o ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 |
35 | 24, 34 | jctil 312 |
. 2
⊢ (¬
¬ 𝜑 → (∀𝑎 ∈ 2o ¬
𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ∧ ∀𝑎 ∈ 2o ∀𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎))) |
36 | 9 | 3adant3 1017 |
. . . . . 6
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
37 | | simpr 110 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ 𝑎 = 𝑐) → 𝑎 = 𝑐) |
38 | | simplrr 536 |
. . . . . . . . . . . 12
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ 𝑎 = 𝑐) → 𝑎 ≠ 𝑏) |
39 | 37, 38 | eqnetrrd 2373 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ 𝑎 = 𝑐) → 𝑐 ≠ 𝑏) |
40 | 39 | necomd 2433 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ 𝑎 = 𝑐) → 𝑏 ≠ 𝑐) |
41 | 40 | olcd 734 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ 𝑎 = 𝑐) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
42 | | simpr 110 |
. . . . . . . . . . 11
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ ¬ 𝑎 = 𝑐) → ¬ 𝑎 = 𝑐) |
43 | 42 | neqned 2354 |
. . . . . . . . . 10
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ ¬ 𝑎 = 𝑐) → 𝑎 ≠ 𝑐) |
44 | 43 | orcd 733 |
. . . . . . . . 9
⊢ ((((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) ∧ ¬ 𝑎 = 𝑐) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
45 | | simpl1 1000 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → 𝑎 ∈ 2o) |
46 | | 2onn 6522 |
. . . . . . . . . . . 12
⊢
2o ∈ ω |
47 | | elnn 4606 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 2o ∧
2o ∈ ω) → 𝑎 ∈ ω) |
48 | 45, 46, 47 | sylancl 413 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → 𝑎 ∈ ω) |
49 | | simpl3 1002 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → 𝑐 ∈ 2o) |
50 | | elnn 4606 |
. . . . . . . . . . . 12
⊢ ((𝑐 ∈ 2o ∧
2o ∈ ω) → 𝑐 ∈ ω) |
51 | 49, 46, 50 | sylancl 413 |
. . . . . . . . . . 11
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → 𝑐 ∈ ω) |
52 | | nndceq 6500 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ ω ∧ 𝑐 ∈ ω) →
DECID 𝑎 =
𝑐) |
53 | 48, 51, 52 | syl2anc 411 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → DECID 𝑎 = 𝑐) |
54 | | exmiddc 836 |
. . . . . . . . . 10
⊢
(DECID 𝑎 = 𝑐 → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐)) |
55 | 53, 54 | syl 14 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐)) |
56 | 41, 44, 55 | mpjaodan 798 |
. . . . . . . 8
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
57 | | df-br 4005 |
. . . . . . . . . . . 12
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ ⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
58 | | neeq2 2361 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑐 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑐)) |
59 | 58 | anbi2d 464 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑐 → ((𝜑 ∧ 𝑎 ≠ 𝑣) ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
60 | 5, 59 | opelopab2 4271 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ 2o ∧
𝑐 ∈ 2o)
→ (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
61 | 60 | 3adant2 1016 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
62 | 57, 61 | bitrid 192 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
63 | 62 | adantr 276 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
64 | | ibar 301 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑎 ≠ 𝑐 ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
65 | 64 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → (𝑎 ≠ 𝑐 ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
66 | 65 | adantl 277 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎 ≠ 𝑐 ↔ (𝜑 ∧ 𝑎 ≠ 𝑐))) |
67 | 63, 66 | bitr4d 191 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ 𝑎 ≠ 𝑐)) |
68 | | df-br 4005 |
. . . . . . . . . . . 12
⊢ (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ ⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}) |
69 | | neeq2 2361 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑐 → (𝑏 ≠ 𝑣 ↔ 𝑏 ≠ 𝑐)) |
70 | 69 | anbi2d 464 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑐 → ((𝜑 ∧ 𝑏 ≠ 𝑣) ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
71 | 12, 70 | opelopab2 4271 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 2o ∧
𝑐 ∈ 2o)
→ (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
72 | 71 | 3adant1 1015 |
. . . . . . . . . . . 12
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
73 | 68, 72 | bitrid 192 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
74 | 73 | adantr 276 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
75 | | ibar 301 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ≠ 𝑐 ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
76 | 75 | adantr 276 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) → (𝑏 ≠ 𝑐 ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
77 | 76 | adantl 277 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑏 ≠ 𝑐 ↔ (𝜑 ∧ 𝑏 ≠ 𝑐))) |
78 | 74, 77 | bitr4d 191 |
. . . . . . . . 9
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ↔ 𝑏 ≠ 𝑐)) |
79 | 67, 78 | orbi12d 793 |
. . . . . . . 8
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → ((𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐) ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐))) |
80 | 56, 79 | mpbird 167 |
. . . . . . 7
⊢ (((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) ∧ (𝜑 ∧
𝑎 ≠ 𝑏)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐)) |
81 | 80 | ex 115 |
. . . . . 6
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → ((𝜑
∧ 𝑎 ≠ 𝑏) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐))) |
82 | 36, 81 | sylbid 150 |
. . . . 5
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐))) |
83 | 82 | adantl 277 |
. . . 4
⊢ ((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o
∧ 𝑐 ∈
2o)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐))) |
84 | 83 | ralrimivvva 2560 |
. . 3
⊢ (¬
¬ 𝜑 → ∀𝑎 ∈ 2o
∀𝑏 ∈
2o ∀𝑐
∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐))) |
85 | 9 | notbid 667 |
. . . . . 6
⊢ ((𝑎 ∈ 2o ∧
𝑏 ∈ 2o)
→ (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
86 | 85 | adantl 277 |
. . . . 5
⊢ ((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
→ (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 ↔ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏))) |
87 | | simpll 527 |
. . . . . . . 8
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → ¬ ¬ 𝜑) |
88 | | simpr 110 |
. . . . . . . . . 10
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) |
89 | | ancom 266 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ≠ 𝑏) ↔ (𝑎 ≠ 𝑏 ∧ 𝜑)) |
90 | 88, 89 | sylnib 676 |
. . . . . . . . 9
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → ¬ (𝑎 ≠ 𝑏 ∧ 𝜑)) |
91 | | imnan 690 |
. . . . . . . . 9
⊢ ((𝑎 ≠ 𝑏 → ¬ 𝜑) ↔ ¬ (𝑎 ≠ 𝑏 ∧ 𝜑)) |
92 | 90, 91 | sylibr 134 |
. . . . . . . 8
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → (𝑎 ≠ 𝑏 → ¬ 𝜑)) |
93 | 87, 92 | mtod 663 |
. . . . . . 7
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → ¬ 𝑎 ≠ 𝑏) |
94 | | simplrl 535 |
. . . . . . . . . 10
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ 2o) |
95 | 94, 46, 47 | sylancl 413 |
. . . . . . . . 9
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → 𝑎 ∈ ω) |
96 | | simplrr 536 |
. . . . . . . . . 10
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ 2o) |
97 | | elnn 4606 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 2o ∧
2o ∈ ω) → 𝑏 ∈ ω) |
98 | 96, 46, 97 | sylancl 413 |
. . . . . . . . 9
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → 𝑏 ∈ ω) |
99 | | nndceq 6500 |
. . . . . . . . 9
⊢ ((𝑎 ∈ ω ∧ 𝑏 ∈ ω) →
DECID 𝑎 =
𝑏) |
100 | 95, 98, 99 | syl2anc 411 |
. . . . . . . 8
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → DECID 𝑎 = 𝑏) |
101 | | nnedc 2352 |
. . . . . . . 8
⊢
(DECID 𝑎 = 𝑏 → (¬ 𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏)) |
102 | 100, 101 | syl 14 |
. . . . . . 7
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → (¬ 𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏)) |
103 | 93, 102 | mpbid 147 |
. . . . . 6
⊢ (((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
∧ ¬ (𝜑 ∧ 𝑎 ≠ 𝑏)) → 𝑎 = 𝑏) |
104 | 103 | ex 115 |
. . . . 5
⊢ ((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
→ (¬ (𝜑 ∧ 𝑎 ≠ 𝑏) → 𝑎 = 𝑏)) |
105 | 86, 104 | sylbid 150 |
. . . 4
⊢ ((¬
¬ 𝜑 ∧ (𝑎 ∈ 2o ∧
𝑏 ∈ 2o))
→ (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑎 = 𝑏)) |
106 | 105 | ralrimivva 2559 |
. . 3
⊢ (¬
¬ 𝜑 → ∀𝑎 ∈ 2o
∀𝑏 ∈
2o (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑎 = 𝑏)) |
107 | 84, 106 | jca 306 |
. 2
⊢ (¬
¬ 𝜑 → (∀𝑎 ∈ 2o
∀𝑏 ∈
2o ∀𝑐
∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐)) ∧ ∀𝑎 ∈ 2o ∀𝑏 ∈ 2o (¬
𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑎 = 𝑏))) |
108 | | dftap2 7250 |
. 2
⊢
({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧
𝑣 ∈ 2o)
∧ (𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o ↔ ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} ⊆ (2o ×
2o) ∧ (∀𝑎 ∈ 2o ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎 ∧ ∀𝑎 ∈ 2o ∀𝑏 ∈ 2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑎)) ∧ (∀𝑎 ∈ 2o ∀𝑏 ∈ 2o
∀𝑐 ∈
2o (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑐)) ∧ ∀𝑎 ∈ 2o ∀𝑏 ∈ 2o (¬
𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))}𝑏 → 𝑎 = 𝑏)))) |
109 | 2, 35, 107, 108 | syl3anbrc 1181 |
1
⊢ (¬
¬ 𝜑 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 2o ∧ 𝑣 ∈ 2o) ∧
(𝜑 ∧ 𝑢 ≠ 𝑣))} TAp 2o) |