Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . 5
⊢
(SymGrp‘{𝐽}) =
(SymGrp‘{𝐽}) |
2 | | eqid 2737 |
. . . . 5
⊢
(Base‘(SymGrp‘{𝐽})) = (Base‘(SymGrp‘{𝐽})) |
3 | | eqid 2737 |
. . . . 5
⊢ {𝐽} = {𝐽} |
4 | 1, 2, 3 | symg1bas 19179 |
. . . 4
⊢ (𝐽 ∈ 𝑊 → (Base‘(SymGrp‘{𝐽})) = {{⟨𝐽, 𝐽⟩}}) |
5 | 4 | ad2antll 728 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘(SymGrp‘{𝐽})) = {{⟨𝐽, 𝐽⟩}}) |
6 | | symg1bas.2 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
7 | | symg1bas.1 |
. . . . . 6
⊢ 𝐺 = (SymGrp‘𝐴) |
8 | | symg2bas.0 |
. . . . . . . 8
⊢ 𝐴 = {𝐼, 𝐽} |
9 | | df-pr 4594 |
. . . . . . . . 9
⊢ {𝐼, 𝐽} = ({𝐼} ∪ {𝐽}) |
10 | | sneq 4601 |
. . . . . . . . . . . 12
⊢ (𝐼 = 𝐽 → {𝐼} = {𝐽}) |
11 | 10 | uneq1d 4127 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝐽 → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
12 | 11 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
13 | | unidm 4117 |
. . . . . . . . . 10
⊢ ({𝐽} ∪ {𝐽}) = {𝐽} |
14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = {𝐽}) |
15 | 9, 14 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {𝐼, 𝐽} = {𝐽}) |
16 | 8, 15 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐴 = {𝐽}) |
17 | 16 | fveq2d 6851 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (SymGrp‘𝐴) = (SymGrp‘{𝐽})) |
18 | 7, 17 | eqtrid 2789 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐺 = (SymGrp‘{𝐽})) |
19 | 18 | fveq2d 6851 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘𝐺) = (Base‘(SymGrp‘{𝐽}))) |
20 | 6, 19 | eqtrid 2789 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = (Base‘(SymGrp‘{𝐽}))) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝐼 = 𝐽 → 𝐼 = 𝐽) |
22 | 21, 21 | opeq12d 4843 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → ⟨𝐼, 𝐼⟩ = ⟨𝐽, 𝐽⟩) |
23 | 22 | adantr 482 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ⟨𝐼, 𝐼⟩ = ⟨𝐽, 𝐽⟩) |
24 | 23 | preq1d 4705 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩, ⟨𝐽, 𝐽⟩}) |
25 | | eqid 2737 |
. . . . . . 7
⊢
⟨𝐽, 𝐽⟩ = ⟨𝐽, 𝐽⟩ |
26 | | opex 5426 |
. . . . . . . 8
⊢
⟨𝐽, 𝐽⟩ ∈ V |
27 | 26, 26 | preqsn 4824 |
. . . . . . 7
⊢
({⟨𝐽, 𝐽⟩, ⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩} ↔ (⟨𝐽, 𝐽⟩ = ⟨𝐽, 𝐽⟩ ∧ ⟨𝐽, 𝐽⟩ = ⟨𝐽, 𝐽⟩)) |
28 | 25, 25, 27 | mpbir2an 710 |
. . . . . 6
⊢
{⟨𝐽, 𝐽⟩, ⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩} |
29 | 24, 28 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩}) |
30 | | opeq1 4835 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → ⟨𝐼, 𝐽⟩ = ⟨𝐽, 𝐽⟩) |
31 | | opeq2 4836 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → ⟨𝐽, 𝐼⟩ = ⟨𝐽, 𝐽⟩) |
32 | 30, 31 | preq12d 4707 |
. . . . . . 7
⊢ (𝐼 = 𝐽 → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} = {⟨𝐽, 𝐽⟩, ⟨𝐽, 𝐽⟩}) |
33 | 32, 28 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐼 = 𝐽 → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} = {⟨𝐽, 𝐽⟩}) |
34 | 33 | adantr 482 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} = {⟨𝐽, 𝐽⟩}) |
35 | 29, 34 | preq12d 4707 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}} = {{⟨𝐽, 𝐽⟩}, {⟨𝐽, 𝐽⟩}}) |
36 | | eqid 2737 |
. . . . 5
⊢
{⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩} |
37 | | snex 5393 |
. . . . . 6
⊢
{⟨𝐽, 𝐽⟩} ∈
V |
38 | 37, 37 | preqsn 4824 |
. . . . 5
⊢
({{⟨𝐽, 𝐽⟩}, {⟨𝐽, 𝐽⟩}} = {{⟨𝐽, 𝐽⟩}} ↔ ({⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩} ∧ {⟨𝐽, 𝐽⟩} = {⟨𝐽, 𝐽⟩})) |
39 | 36, 36, 38 | mpbir2an 710 |
. . . 4
⊢
{{⟨𝐽, 𝐽⟩}, {⟨𝐽, 𝐽⟩}} = {{⟨𝐽, 𝐽⟩}} |
40 | 35, 39 | eqtrdi 2793 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}} = {{⟨𝐽, 𝐽⟩}}) |
41 | 5, 20, 40 | 3eqtr4d 2787 |
. 2
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}}) |
42 | 6 | fvexi 6861 |
. . . 4
⊢ 𝐵 ∈ V |
43 | 42 | a1i 11 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 ∈ V) |
44 | | neqne 2952 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → 𝐼 ≠ 𝐽) |
45 | 44 | anim2i 618 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
46 | | df-3an 1090 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) ↔ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
47 | 45, 46 | sylibr 233 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
48 | 47 | ancoms 460 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
49 | 7, 6, 8 | symg2hash 19180 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2) |
50 | 48, 49 | syl 17 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (♯‘𝐵) = 2) |
51 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
52 | 51 | ancri 551 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
53 | | id 22 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑊 → 𝐽 ∈ 𝑊) |
54 | 53 | ancri 551 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑊 → (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) |
55 | 52, 54 | anim12i 614 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊))) |
56 | | df-ne 2945 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) |
57 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽) |
58 | 57 | ancri 551 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
59 | 56, 58 | sylbir 234 |
. . . . . 6
⊢ (¬
𝐼 = 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
60 | | f1oprg 6834 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) → ((𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
61 | 60 | imp 408 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) ∧ (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
62 | 55, 59, 61 | syl2anr 598 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
63 | | eqidd 2738 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} = {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}) |
64 | | id 22 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → 𝐴 = {𝐼, 𝐽}) |
65 | 63, 64, 64 | f1oeq123d 6783 |
. . . . . 6
⊢ (𝐴 = {𝐼, 𝐽} → ({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:𝐴–1-1-onto→𝐴 ↔ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
66 | 8, 65 | ax-mp 5 |
. . . . 5
⊢
({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:𝐴–1-1-onto→𝐴 ↔ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
67 | 62, 66 | sylibr 233 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:𝐴–1-1-onto→𝐴) |
68 | | prex 5394 |
. . . . 5
⊢
{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ V |
69 | 7, 6 | elsymgbas2 19161 |
. . . . 5
⊢
({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ V → ({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ 𝐵 ↔ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:𝐴–1-1-onto→𝐴)) |
70 | 68, 69 | ax-mp 5 |
. . . 4
⊢
({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ 𝐵 ↔ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}:𝐴–1-1-onto→𝐴) |
71 | 67, 70 | sylibr 233 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ 𝐵) |
72 | | f1oprswap 6833 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
73 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝐴 = {𝐼, 𝐽} → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} = {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}) |
74 | 73, 64, 64 | f1oeq123d 6783 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → ({⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴 ↔ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
75 | 8, 74 | ax-mp 5 |
. . . . . 6
⊢
({⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴 ↔ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
76 | 72, 75 | sylibr 233 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴) |
77 | 76 | adantl 483 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴) |
78 | | prex 5394 |
. . . . 5
⊢
{⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ V |
79 | 7, 6 | elsymgbas2 19161 |
. . . . 5
⊢
({⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ V → ({⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ 𝐵 ↔ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴)) |
80 | 78, 79 | ax-mp 5 |
. . . 4
⊢
({⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ 𝐵 ↔ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}:𝐴–1-1-onto→𝐴) |
81 | 77, 80 | sylibr 233 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ 𝐵) |
82 | | opex 5426 |
. . . . . 6
⊢
⟨𝐼, 𝐼⟩ ∈ V |
83 | 82, 26 | pm3.2i 472 |
. . . . 5
⊢
(⟨𝐼, 𝐼⟩ ∈ V ∧
⟨𝐽, 𝐽⟩ ∈ V) |
84 | | opex 5426 |
. . . . . 6
⊢
⟨𝐼, 𝐽⟩ ∈ V |
85 | | opex 5426 |
. . . . . 6
⊢
⟨𝐽, 𝐼⟩ ∈ V |
86 | 84, 85 | pm3.2i 472 |
. . . . 5
⊢
(⟨𝐼, 𝐽⟩ ∈ V ∧
⟨𝐽, 𝐼⟩ ∈ V) |
87 | 83, 86 | pm3.2i 472 |
. . . 4
⊢
((⟨𝐼, 𝐼⟩ ∈ V ∧
⟨𝐽, 𝐽⟩ ∈ V) ∧ (⟨𝐼, 𝐽⟩ ∈ V ∧ ⟨𝐽, 𝐼⟩ ∈ V)) |
88 | | opthg2 5441 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (⟨𝐼, 𝐼⟩ = ⟨𝐼, 𝐽⟩ ↔ (𝐼 = 𝐼 ∧ 𝐼 = 𝐽))) |
89 | | eqtr 2760 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐼 ∧ 𝐼 = 𝐽) → 𝐼 = 𝐽) |
90 | 88, 89 | syl6bi 253 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (⟨𝐼, 𝐼⟩ = ⟨𝐼, 𝐽⟩ → 𝐼 = 𝐽)) |
91 | 90 | necon3d 2965 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩)) |
92 | 91 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩)) |
93 | 56, 92 | sylbir 234 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩)) |
94 | 93 | imp 408 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩) |
95 | 52 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
96 | | opthg 5439 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → (⟨𝐼, 𝐼⟩ = ⟨𝐽, 𝐼⟩ ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (⟨𝐼, 𝐼⟩ = ⟨𝐽, 𝐼⟩ ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
98 | | simpl 484 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐽 ∧ 𝐼 = 𝐼) → 𝐼 = 𝐽) |
99 | 97, 98 | syl6bi 253 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (⟨𝐼, 𝐼⟩ = ⟨𝐽, 𝐼⟩ → 𝐼 = 𝐽)) |
100 | 99 | necon3d 2965 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩)) |
101 | 100 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩)) |
102 | 56, 101 | sylbir 234 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩)) |
103 | 102 | imp 408 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩) |
104 | 94, 103 | jca 513 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩ ∧ ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩)) |
105 | 104 | orcd 872 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ((⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩ ∧ ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩) ∨ (⟨𝐽, 𝐽⟩ ≠ ⟨𝐼, 𝐽⟩ ∧ ⟨𝐽, 𝐽⟩ ≠ ⟨𝐽, 𝐼⟩))) |
106 | | prneimg 4817 |
. . . 4
⊢
(((⟨𝐼, 𝐼⟩ ∈ V ∧
⟨𝐽, 𝐽⟩ ∈ V) ∧ (⟨𝐼, 𝐽⟩ ∈ V ∧ ⟨𝐽, 𝐼⟩ ∈ V)) → (((⟨𝐼, 𝐼⟩ ≠ ⟨𝐼, 𝐽⟩ ∧ ⟨𝐼, 𝐼⟩ ≠ ⟨𝐽, 𝐼⟩) ∨ (⟨𝐽, 𝐽⟩ ≠ ⟨𝐼, 𝐽⟩ ∧ ⟨𝐽, 𝐽⟩ ≠ ⟨𝐽, 𝐼⟩)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ≠ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩})) |
107 | 87, 105, 106 | mpsyl 68 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ≠ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}) |
108 | | hash2prd 14381 |
. . . 4
⊢ ((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
→ (({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ 𝐵 ∧ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ 𝐵 ∧ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ≠ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}})) |
109 | 108 | imp 408 |
. . 3
⊢ (((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
∧ ({⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ∈ 𝐵 ∧ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩} ∈ 𝐵 ∧ {⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩} ≠ {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩})) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}}) |
110 | 43, 50, 71, 81, 107, 109 | syl23anc 1378 |
. 2
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}}) |
111 | 41, 110 | pm2.61ian 811 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}}) |