Step | Hyp | Ref
| Expression |
1 | | simplr 528 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → 𝑅 TAp 𝐴) |
2 | | simpr 110 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → 𝑝 ∈ 𝑅) |
3 | | dftap2 7249 |
. . . . . . . . . 10
⊢ (𝑅 TAp 𝐴 ↔ (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))) |
4 | 3 | biimpi 120 |
. . . . . . . . 9
⊢ (𝑅 TAp 𝐴 → (𝑅 ⊆ (𝐴 × 𝐴) ∧ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥)) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)))) |
5 | 4 | simp1d 1009 |
. . . . . . . 8
⊢ (𝑅 TAp 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) |
6 | 5 | sseld 3154 |
. . . . . . 7
⊢ (𝑅 TAp 𝐴 → (𝑝 ∈ 𝑅 → 𝑝 ∈ (𝐴 × 𝐴))) |
7 | 1, 2, 6 | sylc 62 |
. . . . . 6
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → 𝑝 ∈ (𝐴 × 𝐴)) |
8 | | 1st2nd2 6175 |
. . . . . 6
⊢ (𝑝 ∈ (𝐴 × 𝐴) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
9 | 7, 8 | syl 14 |
. . . . 5
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
10 | | xp1st 6165 |
. . . . . . . 8
⊢ (𝑝 ∈ (𝐴 × 𝐴) → (1st ‘𝑝) ∈ 𝐴) |
11 | 7, 10 | syl 14 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → (1st ‘𝑝) ∈ 𝐴) |
12 | | xp2nd 6166 |
. . . . . . . 8
⊢ (𝑝 ∈ (𝐴 × 𝐴) → (2nd ‘𝑝) ∈ 𝐴) |
13 | 7, 12 | syl 14 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → (2nd ‘𝑝) ∈ 𝐴) |
14 | 9, 2 | eqeltrrd 2255 |
. . . . . . . . . 10
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ 𝑅) |
15 | 14 | adantr 276 |
. . . . . . . . 9
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ⟨(1st
‘𝑝), (2nd
‘𝑝)⟩ ∈
𝑅) |
16 | | simpr 110 |
. . . . . . . . . . 11
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → (1st
‘𝑝) = (2nd
‘𝑝)) |
17 | 16 | opeq2d 3785 |
. . . . . . . . . 10
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ⟨(1st
‘𝑝), (1st
‘𝑝)⟩ =
⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
18 | | id 19 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1st ‘𝑝) → 𝑥 = (1st ‘𝑝)) |
19 | 18, 18 | breq12d 4016 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1st ‘𝑝) → (𝑥𝑅𝑥 ↔ (1st ‘𝑝)𝑅(1st ‘𝑝))) |
20 | 19 | notbid 667 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑝) → (¬ 𝑥𝑅𝑥 ↔ ¬ (1st ‘𝑝)𝑅(1st ‘𝑝))) |
21 | 4 | simp2d 1010 |
. . . . . . . . . . . . . 14
⊢ (𝑅 TAp 𝐴 → (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → 𝑦𝑅𝑥))) |
22 | 21 | simpld 112 |
. . . . . . . . . . . . 13
⊢ (𝑅 TAp 𝐴 → ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) |
23 | 22 | ad3antlr 493 |
. . . . . . . . . . . 12
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) |
24 | 11 | adantr 276 |
. . . . . . . . . . . 12
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → (1st
‘𝑝) ∈ 𝐴) |
25 | 20, 23, 24 | rspcdva 2846 |
. . . . . . . . . . 11
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ¬ (1st
‘𝑝)𝑅(1st ‘𝑝)) |
26 | | df-br 4004 |
. . . . . . . . . . 11
⊢
((1st ‘𝑝)𝑅(1st ‘𝑝) ↔ ⟨(1st ‘𝑝), (1st ‘𝑝)⟩ ∈ 𝑅) |
27 | 25, 26 | sylnib 676 |
. . . . . . . . . 10
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ¬
⟨(1st ‘𝑝), (1st ‘𝑝)⟩ ∈ 𝑅) |
28 | 17, 27 | eqneltrrd 2274 |
. . . . . . . . 9
⊢
((((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) ∧ (1st ‘𝑝) = (2nd ‘𝑝)) → ¬
⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ 𝑅) |
29 | 15, 28 | pm2.65da 661 |
. . . . . . . 8
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → ¬ (1st ‘𝑝) = (2nd ‘𝑝)) |
30 | 29 | neqned 2354 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → (1st ‘𝑝) ≠ (2nd
‘𝑝)) |
31 | 11, 13, 30 | jca31 309 |
. . . . . 6
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝))) |
32 | | eleq1 2240 |
. . . . . . . . . 10
⊢ (𝑢 = (1st ‘𝑝) → (𝑢 ∈ 𝐴 ↔ (1st ‘𝑝) ∈ 𝐴)) |
33 | | eleq1 2240 |
. . . . . . . . . 10
⊢ (𝑣 = (2nd ‘𝑝) → (𝑣 ∈ 𝐴 ↔ (2nd ‘𝑝) ∈ 𝐴)) |
34 | 32, 33 | bi2anan9 606 |
. . . . . . . . 9
⊢ ((𝑢 = (1st ‘𝑝) ∧ 𝑣 = (2nd ‘𝑝)) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ↔ ((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴))) |
35 | | simpl 109 |
. . . . . . . . . 10
⊢ ((𝑢 = (1st ‘𝑝) ∧ 𝑣 = (2nd ‘𝑝)) → 𝑢 = (1st ‘𝑝)) |
36 | | simpr 110 |
. . . . . . . . . 10
⊢ ((𝑢 = (1st ‘𝑝) ∧ 𝑣 = (2nd ‘𝑝)) → 𝑣 = (2nd ‘𝑝)) |
37 | 35, 36 | neeq12d 2367 |
. . . . . . . . 9
⊢ ((𝑢 = (1st ‘𝑝) ∧ 𝑣 = (2nd ‘𝑝)) → (𝑢 ≠ 𝑣 ↔ (1st ‘𝑝) ≠ (2nd
‘𝑝))) |
38 | 34, 37 | anbi12d 473 |
. . . . . . . 8
⊢ ((𝑢 = (1st ‘𝑝) ∧ 𝑣 = (2nd ‘𝑝)) → (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) ↔ (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝)))) |
39 | 38 | opelopabga 4263 |
. . . . . . 7
⊢
(((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) → (⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝)))) |
40 | 11, 13, 39 | syl2anc 411 |
. . . . . 6
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → (⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ↔ (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝)))) |
41 | 31, 40 | mpbird 167 |
. . . . 5
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
42 | 9, 41 | eqeltrd 2254 |
. . . 4
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ 𝑅) → 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
43 | | relopab 4753 |
. . . . . . 7
⊢ Rel
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} |
44 | | 1st2nd 6181 |
. . . . . . 7
⊢ ((Rel
{⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
45 | 43, 44 | mpan 424 |
. . . . . 6
⊢ (𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
46 | 45 | adantl 277 |
. . . . 5
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → 𝑝 = ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩) |
47 | | breq2 4007 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑝) → ((1st
‘𝑝)𝑅𝑦 ↔ (1st ‘𝑝)𝑅(2nd ‘𝑝))) |
48 | 47 | notbid 667 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑝) → (¬ (1st
‘𝑝)𝑅𝑦 ↔ ¬ (1st ‘𝑝)𝑅(2nd ‘𝑝))) |
49 | | eqeq2 2187 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑝) → ((1st
‘𝑝) = 𝑦 ↔ (1st
‘𝑝) = (2nd
‘𝑝))) |
50 | 48, 49 | imbi12d 234 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑝) → ((¬ (1st
‘𝑝)𝑅𝑦 → (1st ‘𝑝) = 𝑦) ↔ (¬ (1st ‘𝑝)𝑅(2nd ‘𝑝) → (1st ‘𝑝) = (2nd ‘𝑝)))) |
51 | | breq1 4006 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1st ‘𝑝) → (𝑥𝑅𝑦 ↔ (1st ‘𝑝)𝑅𝑦)) |
52 | 51 | notbid 667 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑝) → (¬ 𝑥𝑅𝑦 ↔ ¬ (1st ‘𝑝)𝑅𝑦)) |
53 | | eqeq1 2184 |
. . . . . . . . . . 11
⊢ (𝑥 = (1st ‘𝑝) → (𝑥 = 𝑦 ↔ (1st ‘𝑝) = 𝑦)) |
54 | 52, 53 | imbi12d 234 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑝) → ((¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) ↔ (¬ (1st ‘𝑝)𝑅𝑦 → (1st ‘𝑝) = 𝑦))) |
55 | 54 | ralbidv 2477 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑝) → (∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (¬ (1st ‘𝑝)𝑅𝑦 → (1st ‘𝑝) = 𝑦))) |
56 | 4 | simp3d 1011 |
. . . . . . . . . . 11
⊢ (𝑅 TAp 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑦𝑅𝑧)) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))) |
57 | 56 | simprd 114 |
. . . . . . . . . 10
⊢ (𝑅 TAp 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)) |
58 | 57 | ad2antlr 489 |
. . . . . . . . 9
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)) |
59 | 32 | anbi1d 465 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑝) → ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ↔ ((1st ‘𝑝) ∈ 𝐴 ∧ 𝑣 ∈ 𝐴))) |
60 | | neeq1 2360 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (1st ‘𝑝) → (𝑢 ≠ 𝑣 ↔ (1st ‘𝑝) ≠ 𝑣)) |
61 | 59, 60 | anbi12d 473 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑝) → (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣) ↔ (((1st ‘𝑝) ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (1st ‘𝑝) ≠ 𝑣))) |
62 | 33 | anbi2d 464 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (2nd ‘𝑝) → (((1st
‘𝑝) ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ↔ ((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴))) |
63 | | neeq2 2361 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = (2nd ‘𝑝) → ((1st
‘𝑝) ≠ 𝑣 ↔ (1st
‘𝑝) ≠
(2nd ‘𝑝))) |
64 | 62, 63 | anbi12d 473 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (2nd ‘𝑝) → ((((1st
‘𝑝) ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ (1st ‘𝑝) ≠ 𝑣) ↔ (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝)))) |
65 | 61, 64 | elopabi 6195 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} → (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝))) |
66 | 65 | adantl 277 |
. . . . . . . . . . 11
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴) ∧ (1st ‘𝑝) ≠ (2nd
‘𝑝))) |
67 | 66 | simpld 112 |
. . . . . . . . . 10
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ((1st ‘𝑝) ∈ 𝐴 ∧ (2nd ‘𝑝) ∈ 𝐴)) |
68 | 67 | simpld 112 |
. . . . . . . . 9
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (1st ‘𝑝) ∈ 𝐴) |
69 | 55, 58, 68 | rspcdva 2846 |
. . . . . . . 8
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ∀𝑦 ∈ 𝐴 (¬ (1st ‘𝑝)𝑅𝑦 → (1st ‘𝑝) = 𝑦)) |
70 | 67 | simprd 114 |
. . . . . . . 8
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (2nd ‘𝑝) ∈ 𝐴) |
71 | 50, 69, 70 | rspcdva 2846 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (¬ (1st
‘𝑝)𝑅(2nd ‘𝑝) → (1st ‘𝑝) = (2nd ‘𝑝))) |
72 | 66 | simprd 114 |
. . . . . . . 8
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (1st ‘𝑝) ≠ (2nd
‘𝑝)) |
73 | 72 | neneqd 2368 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ¬ (1st ‘𝑝) = (2nd ‘𝑝)) |
74 | | exmidexmid 4196 |
. . . . . . . . 9
⊢
(EXMID → DECID (1st
‘𝑝)𝑅(2nd ‘𝑝)) |
75 | | con1dc 856 |
. . . . . . . . 9
⊢
(DECID (1st ‘𝑝)𝑅(2nd ‘𝑝) → ((¬ (1st ‘𝑝)𝑅(2nd ‘𝑝) → (1st ‘𝑝) = (2nd ‘𝑝)) → (¬ (1st
‘𝑝) = (2nd
‘𝑝) →
(1st ‘𝑝)𝑅(2nd ‘𝑝)))) |
76 | 74, 75 | syl 14 |
. . . . . . . 8
⊢
(EXMID → ((¬ (1st ‘𝑝)𝑅(2nd ‘𝑝) → (1st ‘𝑝) = (2nd ‘𝑝)) → (¬ (1st
‘𝑝) = (2nd
‘𝑝) →
(1st ‘𝑝)𝑅(2nd ‘𝑝)))) |
77 | 76 | ad2antrr 488 |
. . . . . . 7
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ((¬ (1st
‘𝑝)𝑅(2nd ‘𝑝) → (1st ‘𝑝) = (2nd ‘𝑝)) → (¬ (1st
‘𝑝) = (2nd
‘𝑝) →
(1st ‘𝑝)𝑅(2nd ‘𝑝)))) |
78 | 71, 73, 77 | mp2d 47 |
. . . . . 6
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (1st ‘𝑝)𝑅(2nd ‘𝑝)) |
79 | | df-br 4004 |
. . . . . 6
⊢
((1st ‘𝑝)𝑅(2nd ‘𝑝) ↔ ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ 𝑅) |
80 | 78, 79 | sylib 122 |
. . . . 5
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → ⟨(1st ‘𝑝), (2nd ‘𝑝)⟩ ∈ 𝑅) |
81 | 46, 80 | eqeltrd 2254 |
. . . 4
⊢
(((EXMID ∧ 𝑅 TAp 𝐴) ∧ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → 𝑝 ∈ 𝑅) |
82 | 42, 81 | impbida 596 |
. . 3
⊢
((EXMID ∧ 𝑅 TAp 𝐴) → (𝑝 ∈ 𝑅 ↔ 𝑝 ∈ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)})) |
83 | 82 | eqrdv 2175 |
. 2
⊢
((EXMID ∧ 𝑅 TAp 𝐴) → 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) |
84 | | exmidexmid 4196 |
. . . . . . 7
⊢
(EXMID → DECID 𝑥 = 𝑦) |
85 | 84 | ralrimivw 2551 |
. . . . . 6
⊢
(EXMID → ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
86 | 85 | ralrimivw 2551 |
. . . . 5
⊢
(EXMID → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦) |
87 | | netap 7252 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴) |
88 | 86, 87 | syl 14 |
. . . 4
⊢
(EXMID → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴) |
89 | 88 | adantr 276 |
. . 3
⊢
((EXMID ∧ 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴) |
90 | | tapeq1 7250 |
. . . 4
⊢ (𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} → (𝑅 TAp 𝐴 ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴)) |
91 | 90 | adantl 277 |
. . 3
⊢
((EXMID ∧ 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → (𝑅 TAp 𝐴 ↔ {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)} TAp 𝐴)) |
92 | 89, 91 | mpbird 167 |
. 2
⊢
((EXMID ∧ 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)}) → 𝑅 TAp 𝐴) |
93 | 83, 92 | impbida 596 |
1
⊢
(EXMID → (𝑅 TAp 𝐴 ↔ 𝑅 = {⟨𝑢, 𝑣⟩ ∣ ((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) ∧ 𝑢 ≠ 𝑣)})) |