Step | Hyp | Ref
| Expression |
1 | | opabssxp 4701 |
. . 3
⊢
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ⊆ (𝐴 × 𝐴) |
2 | 1 | a1i 9 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ⊆ (𝐴 × 𝐴)) |
3 | | neirr 2356 |
. . . . . 6
⊢ ¬
𝑎 ≠ 𝑎 |
4 | | df-br 4005 |
. . . . . . 7
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ↔ ⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
5 | | neeq1 2360 |
. . . . . . . . 9
⊢ (𝑢 = 𝑎 → (𝑢 ≠ 𝑣 ↔ 𝑎 ≠ 𝑣)) |
6 | | neeq2 2361 |
. . . . . . . . 9
⊢ (𝑣 = 𝑎 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑎)) |
7 | 5, 6 | opelopab2 4271 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) → (⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑎)) |
8 | 7 | anidms 397 |
. . . . . . 7
⊢ (𝑎 ∈ 𝐴 → (⟨𝑎, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑎)) |
9 | 4, 8 | bitrid 192 |
. . . . . 6
⊢ (𝑎 ∈ 𝐴 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ↔ 𝑎 ≠ 𝑎)) |
10 | 3, 9 | mtbiri 675 |
. . . . 5
⊢ (𝑎 ∈ 𝐴 → ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎) |
11 | 10 | rgen 2530 |
. . . 4
⊢
∀𝑎 ∈
𝐴 ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 |
12 | 11 | a1i 9 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → ∀𝑎 ∈ 𝐴 ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎) |
13 | | df-br 4005 |
. . . . . . . 8
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
14 | | neeq2 2361 |
. . . . . . . . 9
⊢ (𝑣 = 𝑏 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑏)) |
15 | 5, 14 | opelopab2 4271 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (⟨𝑎, 𝑏⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑏)) |
16 | 13, 15 | bitrid 192 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ 𝑎 ≠ 𝑏)) |
17 | | df-br 4005 |
. . . . . . . 8
⊢ (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ↔ ⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
18 | | neeq1 2360 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑏 → (𝑢 ≠ 𝑣 ↔ 𝑏 ≠ 𝑣)) |
19 | | neeq2 2361 |
. . . . . . . . . . 11
⊢ (𝑣 = 𝑎 → (𝑏 ≠ 𝑣 ↔ 𝑏 ≠ 𝑎)) |
20 | 18, 19 | opelopab2 4271 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑏 ≠ 𝑎)) |
21 | 20 | ancoms 268 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑏 ≠ 𝑎)) |
22 | | necom 2431 |
. . . . . . . . 9
⊢ (𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏) |
23 | 21, 22 | bitrdi 196 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (⟨𝑏, 𝑎⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑏)) |
24 | 17, 23 | bitrid 192 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ↔ 𝑎 ≠ 𝑏)) |
25 | 16, 24 | bitr4d 191 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎)) |
26 | 25 | biimpd 144 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎)) |
27 | 26 | rgen2 2563 |
. . . 4
⊢
∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎) |
28 | 27 | a1i 9 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎)) |
29 | 12, 28 | jca 306 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → (∀𝑎 ∈ 𝐴 ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎))) |
30 | 16 | 3adant3 1017 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ 𝑎 ≠ 𝑏)) |
31 | 30 | adantl 277 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ 𝑎 ≠ 𝑏)) |
32 | | simpr 110 |
. . . . . . . . . . 11
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑎 = 𝑐) → 𝑎 = 𝑐) |
33 | | simplr 528 |
. . . . . . . . . . 11
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑎 = 𝑐) → 𝑎 ≠ 𝑏) |
34 | 32, 33 | eqnetrrd 2373 |
. . . . . . . . . 10
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑎 = 𝑐) → 𝑐 ≠ 𝑏) |
35 | 34 | necomd 2433 |
. . . . . . . . 9
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑎 = 𝑐) → 𝑏 ≠ 𝑐) |
36 | 35 | olcd 734 |
. . . . . . . 8
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ 𝑎 = 𝑐) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
37 | | simpr 110 |
. . . . . . . . . 10
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ ¬ 𝑎 = 𝑐) → ¬ 𝑎 = 𝑐) |
38 | 37 | neqned 2354 |
. . . . . . . . 9
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ ¬ 𝑎 = 𝑐) → 𝑎 ≠ 𝑐) |
39 | 38 | orcd 733 |
. . . . . . . 8
⊢
((((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) ∧ ¬ 𝑎 = 𝑐) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
40 | | equequ2 1713 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑐 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑐)) |
41 | 40 | dcbid 838 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑐 → (DECID 𝑎 = 𝑦 ↔ DECID 𝑎 = 𝑐)) |
42 | | equequ1 1712 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (𝑥 = 𝑦 ↔ 𝑎 = 𝑦)) |
43 | 42 | dcbid 838 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑎 → (DECID 𝑥 = 𝑦 ↔ DECID 𝑎 = 𝑦)) |
44 | 43 | ralbidv 2477 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑎 → (∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ↔ ∀𝑦 ∈ 𝐴 DECID 𝑎 = 𝑦)) |
45 | | simpll 527 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
46 | | simplr1 1039 |
. . . . . . . . . . 11
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → 𝑎 ∈ 𝐴) |
47 | 44, 45, 46 | rspcdva 2847 |
. . . . . . . . . 10
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → ∀𝑦 ∈ 𝐴 DECID 𝑎 = 𝑦) |
48 | | simplr3 1041 |
. . . . . . . . . 10
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → 𝑐 ∈ 𝐴) |
49 | 41, 47, 48 | rspcdva 2847 |
. . . . . . . . 9
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → DECID 𝑎 = 𝑐) |
50 | | exmiddc 836 |
. . . . . . . . 9
⊢
(DECID 𝑎 = 𝑐 → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐)) |
51 | 49, 50 | syl 14 |
. . . . . . . 8
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → (𝑎 = 𝑐 ∨ ¬ 𝑎 = 𝑐)) |
52 | 36, 39, 51 | mpjaodan 798 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐)) |
53 | | df-br 4005 |
. . . . . . . . . 10
⊢ (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ↔ ⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
54 | | neeq2 2361 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑐 → (𝑎 ≠ 𝑣 ↔ 𝑎 ≠ 𝑐)) |
55 | 5, 54 | opelopab2 4271 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑐)) |
56 | 55 | 3adant2 1016 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (⟨𝑎, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑎 ≠ 𝑐)) |
57 | 53, 56 | bitrid 192 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ↔ 𝑎 ≠ 𝑐)) |
58 | | df-br 4005 |
. . . . . . . . . 10
⊢ (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ↔ ⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
59 | | neeq2 2361 |
. . . . . . . . . . . 12
⊢ (𝑣 = 𝑐 → (𝑏 ≠ 𝑣 ↔ 𝑏 ≠ 𝑐)) |
60 | 18, 59 | opelopab2 4271 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑏 ≠ 𝑐)) |
61 | 60 | 3adant1 1015 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (⟨𝑏, 𝑐⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ 𝑏 ≠ 𝑐)) |
62 | 58, 61 | bitrid 192 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → (𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ↔ 𝑏 ≠ 𝑐)) |
63 | 57, 62 | orbi12d 793 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) → ((𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐) ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐))) |
64 | 63 | ad2antlr 489 |
. . . . . . 7
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → ((𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐) ↔ (𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑐))) |
65 | 52, 64 | mpbird 167 |
. . . . . 6
⊢
(((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) ∧ 𝑎 ≠ 𝑏) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐)) |
66 | 65 | ex 115 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎 ≠ 𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐))) |
67 | 31, 66 | sylbid 150 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴)) → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐))) |
68 | 67 | ralrimivvva 2560 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐))) |
69 | 16 | notbid 667 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ ¬ 𝑎 ≠ 𝑏)) |
70 | | df-ne 2348 |
. . . . . . . 8
⊢ (𝑎 ≠ 𝑏 ↔ ¬ 𝑎 = 𝑏) |
71 | 70 | notbii 668 |
. . . . . . 7
⊢ (¬
𝑎 ≠ 𝑏 ↔ ¬ ¬ 𝑎 = 𝑏) |
72 | 69, 71 | bitrdi 196 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ ¬ ¬ 𝑎 = 𝑏)) |
73 | 72 | adantl 277 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 ↔ ¬ ¬ 𝑎 = 𝑏)) |
74 | | equequ2 1713 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → (𝑎 = 𝑦 ↔ 𝑎 = 𝑏)) |
75 | 74 | dcbid 838 |
. . . . . . 7
⊢ (𝑦 = 𝑏 → (DECID 𝑎 = 𝑦 ↔ DECID 𝑎 = 𝑏)) |
76 | | simpl 109 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
77 | | simprl 529 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑎 ∈ 𝐴) |
78 | 44, 76, 77 | rspcdva 2847 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ∀𝑦 ∈ 𝐴 DECID 𝑎 = 𝑦) |
79 | | simprr 531 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏 ∈ 𝐴) |
80 | 75, 78, 79 | rspcdva 2847 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → DECID 𝑎 = 𝑏) |
81 | | notnotrdc 843 |
. . . . . 6
⊢
(DECID 𝑎 = 𝑏 → (¬ ¬ 𝑎 = 𝑏 → 𝑎 = 𝑏)) |
82 | 80, 81 | syl 14 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ ¬ 𝑎 = 𝑏 → 𝑎 = 𝑏)) |
83 | 73, 82 | sylbid 150 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑎 = 𝑏)) |
84 | 83 | ralrimivva 2559 |
. . 3
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑎 = 𝑏)) |
85 | 68, 84 | jca 306 |
. 2
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐)) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑎 = 𝑏))) |
86 | | dftap2 7250 |
. 2
⊢
({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴 ↔ ({⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ⊆ (𝐴 × 𝐴) ∧ (∀𝑎 ∈ 𝐴 ¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑎)) ∧ (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → (𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐 ∨ 𝑏{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑐)) ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (¬ 𝑎{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}𝑏 → 𝑎 = 𝑏)))) |
87 | 2, 29, 85, 86 | syl3anbrc 1181 |
1
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴) |