Proof of Theorem symg2bas
Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . 5
⊢
(SymGrp‘{𝐽}) =
(SymGrp‘{𝐽}) |
2 | | eqid 2738 |
. . . . 5
⊢
(Base‘(SymGrp‘{𝐽})) = (Base‘(SymGrp‘{𝐽})) |
3 | | eqid 2738 |
. . . . 5
⊢ {𝐽} = {𝐽} |
4 | 1, 2, 3 | symg1bas 18998 |
. . . 4
⊢ (𝐽 ∈ 𝑊 → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
5 | 4 | ad2antll 726 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
6 | | symg1bas.2 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
7 | | symg1bas.1 |
. . . . . 6
⊢ 𝐺 = (SymGrp‘𝐴) |
8 | | symg2bas.0 |
. . . . . . . 8
⊢ 𝐴 = {𝐼, 𝐽} |
9 | | df-pr 4564 |
. . . . . . . . 9
⊢ {𝐼, 𝐽} = ({𝐼} ∪ {𝐽}) |
10 | | sneq 4571 |
. . . . . . . . . . . 12
⊢ (𝐼 = 𝐽 → {𝐼} = {𝐽}) |
11 | 10 | uneq1d 4096 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝐽 → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
12 | 11 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
13 | | unidm 4086 |
. . . . . . . . . 10
⊢ ({𝐽} ∪ {𝐽}) = {𝐽} |
14 | 12, 13 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = {𝐽}) |
15 | 9, 14 | eqtrid 2790 |
. . . . . . . 8
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {𝐼, 𝐽} = {𝐽}) |
16 | 8, 15 | eqtrid 2790 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐴 = {𝐽}) |
17 | 16 | fveq2d 6778 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (SymGrp‘𝐴) = (SymGrp‘{𝐽})) |
18 | 7, 17 | eqtrid 2790 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐺 = (SymGrp‘{𝐽})) |
19 | 18 | fveq2d 6778 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘𝐺) = (Base‘(SymGrp‘{𝐽}))) |
20 | 6, 19 | eqtrid 2790 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = (Base‘(SymGrp‘{𝐽}))) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝐼 = 𝐽 → 𝐼 = 𝐽) |
22 | 21, 21 | opeq12d 4812 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
23 | 22 | adantr 481 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
24 | 23 | preq1d 4675 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
25 | | eqid 2738 |
. . . . . . 7
⊢
〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 |
26 | | opex 5379 |
. . . . . . . 8
⊢
〈𝐽, 𝐽〉 ∈ V |
27 | 26, 26 | preqsn 4792 |
. . . . . . 7
⊢
({〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ↔ (〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 ∧ 〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉)) |
28 | 25, 25, 27 | mpbir2an 708 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
29 | 24, 28 | eqtrdi 2794 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉}) |
30 | | opeq1 4804 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐽〉 = 〈𝐽, 𝐽〉) |
31 | | opeq2 4805 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐽, 𝐼〉 = 〈𝐽, 𝐽〉) |
32 | 30, 31 | preq12d 4677 |
. . . . . . 7
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
33 | 32, 28 | eqtrdi 2794 |
. . . . . 6
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
34 | 33 | adantr 481 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
35 | 29, 34 | preq12d 4677 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}}) |
36 | | eqid 2738 |
. . . . 5
⊢
{〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
37 | | snex 5354 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉} ∈
V |
38 | 37, 37 | preqsn 4792 |
. . . . 5
⊢
({{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} ↔ ({〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ∧ {〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉})) |
39 | 36, 36, 38 | mpbir2an 708 |
. . . 4
⊢
{{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} |
40 | 35, 39 | eqtrdi 2794 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}}) |
41 | 5, 20, 40 | 3eqtr4d 2788 |
. 2
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
42 | 6 | fvexi 6788 |
. . . 4
⊢ 𝐵 ∈ V |
43 | 42 | a1i 11 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 ∈ V) |
44 | | neqne 2951 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → 𝐼 ≠ 𝐽) |
45 | 44 | anim2i 617 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
46 | | df-3an 1088 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) ↔ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
47 | 45, 46 | sylibr 233 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
48 | 47 | ancoms 459 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
49 | 7, 6, 8 | symg2hash 18999 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2) |
50 | 48, 49 | syl 17 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (♯‘𝐵) = 2) |
51 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
52 | 51 | ancri 550 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
53 | | id 22 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑊 → 𝐽 ∈ 𝑊) |
54 | 53 | ancri 550 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑊 → (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) |
55 | 52, 54 | anim12i 613 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊))) |
56 | | df-ne 2944 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) |
57 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽) |
58 | 57 | ancri 550 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
59 | 56, 58 | sylbir 234 |
. . . . . 6
⊢ (¬
𝐼 = 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
60 | | f1oprg 6761 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) → ((𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
61 | 60 | imp 407 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) ∧ (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
62 | 55, 59, 61 | syl2anr 597 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
63 | | eqidd 2739 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}) |
64 | | id 22 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → 𝐴 = {𝐼, 𝐽}) |
65 | 63, 64, 64 | f1oeq123d 6710 |
. . . . . 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 5355 |
. . . . 5
⊢
{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V |
69 | 7, 6 | elsymgbas2 18980 |
. . . . 5
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V → ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴)) |
70 | 68, 69 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴) |
71 | 67, 70 | sylibr 233 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵) |
72 | | f1oprswap 6760 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
73 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
74 | 73, 64, 64 | f1oeq123d 6710 |
. . . . . . 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 482 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
78 | | prex 5355 |
. . . . 5
⊢
{〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V |
79 | 7, 6 | elsymgbas2 18980 |
. . . . 5
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V → ({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴)) |
80 | 78, 79 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
81 | 77, 80 | sylibr 233 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵) |
82 | | opex 5379 |
. . . . . 6
⊢
〈𝐼, 𝐼〉 ∈ V |
83 | 82, 26 | pm3.2i 471 |
. . . . 5
⊢
(〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) |
84 | | opex 5379 |
. . . . . 6
⊢
〈𝐼, 𝐽〉 ∈ V |
85 | | opex 5379 |
. . . . . 6
⊢
〈𝐽, 𝐼〉 ∈ V |
86 | 84, 85 | pm3.2i 471 |
. . . . 5
⊢
(〈𝐼, 𝐽〉 ∈ V ∧
〈𝐽, 𝐼〉 ∈ V) |
87 | 83, 86 | pm3.2i 471 |
. . . 4
⊢
((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) |
88 | | opthg2 5394 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 ↔ (𝐼 = 𝐼 ∧ 𝐼 = 𝐽))) |
89 | | eqtr 2761 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐼 ∧ 𝐼 = 𝐽) → 𝐼 = 𝐽) |
90 | 88, 89 | syl6bi 252 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 → 𝐼 = 𝐽)) |
91 | 90 | necon3d 2964 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
92 | 91 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
93 | 56, 92 | sylbir 234 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
94 | 93 | imp 407 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉) |
95 | 52 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
96 | | opthg 5392 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
98 | | simpl 483 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐽 ∧ 𝐼 = 𝐼) → 𝐼 = 𝐽) |
99 | 97, 98 | syl6bi 252 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 → 𝐼 = 𝐽)) |
100 | 99 | necon3d 2964 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
101 | 100 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
102 | 56, 101 | sylbir 234 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
103 | 102 | imp 407 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) |
104 | 94, 103 | jca 512 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
105 | 104 | orcd 870 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉))) |
106 | | prneimg 4785 |
. . . 4
⊢
(((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) → (((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) |
107 | 87, 105, 106 | mpsyl 68 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
108 | | hash2prd 14189 |
. . . 4
⊢ ((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
→ (({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}})) |
109 | 108 | imp 407 |
. . 3
⊢ (((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
∧ ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
110 | 43, 50, 71, 81, 107, 109 | syl23anc 1376 |
. 2
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
111 | 41, 110 | pm2.61ian 809 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |