Proof of Theorem symg2bas
Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢
(SymGrp‘{𝐽}) =
(SymGrp‘{𝐽}) |
2 | | eqid 2610 |
. . . . 5
⊢
(Base‘(SymGrp‘{𝐽})) = (Base‘(SymGrp‘{𝐽})) |
3 | | eqid 2610 |
. . . . 5
⊢ {𝐽} = {𝐽} |
4 | 1, 2, 3 | symg1bas 17639 |
. . . 4
⊢ (𝐽 ∈ 𝑊 → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
5 | 4 | ad2antll 761 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
6 | | symg1bas.2 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
7 | | symg1bas.1 |
. . . . . 6
⊢ 𝐺 = (SymGrp‘𝐴) |
8 | | symg2bas.0 |
. . . . . . . 8
⊢ 𝐴 = {𝐼, 𝐽} |
9 | | df-pr 4128 |
. . . . . . . . 9
⊢ {𝐼, 𝐽} = ({𝐼} ∪ {𝐽}) |
10 | | sneq 4135 |
. . . . . . . . . . . 12
⊢ (𝐼 = 𝐽 → {𝐼} = {𝐽}) |
11 | 10 | uneq1d 3728 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝐽 → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
13 | | unidm 3718 |
. . . . . . . . . 10
⊢ ({𝐽} ∪ {𝐽}) = {𝐽} |
14 | 12, 13 | syl6eq 2660 |
. . . . . . . . 9
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = {𝐽}) |
15 | 9, 14 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {𝐼, 𝐽} = {𝐽}) |
16 | 8, 15 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐴 = {𝐽}) |
17 | 16 | fveq2d 6107 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (SymGrp‘𝐴) = (SymGrp‘{𝐽})) |
18 | 7, 17 | syl5eq 2656 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐺 = (SymGrp‘{𝐽})) |
19 | 18 | fveq2d 6107 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘𝐺) = (Base‘(SymGrp‘{𝐽}))) |
20 | 6, 19 | syl5eq 2656 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = (Base‘(SymGrp‘{𝐽}))) |
21 | | id 22 |
. . . . . . . . 9
⊢ (𝐼 = 𝐽 → 𝐼 = 𝐽) |
22 | 21, 21 | opeq12d 4348 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
24 | 23 | preq1d 4218 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
25 | | eqid 2610 |
. . . . . . 7
⊢
〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 |
26 | | opex 4859 |
. . . . . . . 8
⊢
〈𝐽, 𝐽〉 ∈ V |
27 | 26, 26, 26 | preqsn 4331 |
. . . . . . 7
⊢
({〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ↔ (〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 ∧ 〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉)) |
28 | 25, 25, 27 | mpbir2an 957 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
29 | 24, 28 | syl6eq 2660 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉}) |
30 | | opeq1 4340 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐽〉 = 〈𝐽, 𝐽〉) |
31 | | opeq2 4341 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐽, 𝐼〉 = 〈𝐽, 𝐽〉) |
32 | 30, 31 | preq12d 4220 |
. . . . . . 7
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
33 | 32, 28 | syl6eq 2660 |
. . . . . 6
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
35 | 29, 34 | preq12d 4220 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}}) |
36 | | eqid 2610 |
. . . . 5
⊢
{〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
37 | | snex 4835 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉} ∈
V |
38 | 37, 37, 37 | preqsn 4331 |
. . . . 5
⊢
({{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} ↔ ({〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ∧ {〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉})) |
39 | 36, 36, 38 | mpbir2an 957 |
. . . 4
⊢
{{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} |
40 | 35, 39 | syl6eq 2660 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}}) |
41 | 5, 20, 40 | 3eqtr4d 2654 |
. 2
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
42 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐺)
∈ V |
43 | 6, 42 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
44 | 43 | a1i 11 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 ∈ V) |
45 | | df-ne 2782 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) |
46 | 45 | biimpri 217 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → 𝐼 ≠ 𝐽) |
47 | 46 | anim2i 591 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
48 | | df-3an 1033 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) ↔ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
49 | 47, 48 | sylibr 223 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
50 | 49 | ancoms 468 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
51 | 7, 6, 8 | symg2hash 17640 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (#‘𝐵) = 2) |
52 | 50, 51 | syl 17 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (#‘𝐵) = 2) |
53 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
54 | 53 | ancri 573 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
55 | | id 22 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑊 → 𝐽 ∈ 𝑊) |
56 | 55 | ancri 573 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑊 → (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) |
57 | 54, 56 | anim12i 588 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊))) |
58 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽) |
59 | 58 | ancri 573 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
60 | 45, 59 | sylbir 224 |
. . . . . 6
⊢ (¬
𝐼 = 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
61 | | f1oprg 6093 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) → ((𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
62 | 61 | imp 444 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) ∧ (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
63 | 57, 60, 62 | syl2anr 494 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
64 | | eqidd 2611 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}) |
65 | | id 22 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → 𝐴 = {𝐼, 𝐽}) |
66 | 64, 65, 65 | f1oeq123d 6046 |
. . . . . 6
⊢ (𝐴 = {𝐼, 𝐽} → ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
67 | 8, 66 | ax-mp 5 |
. . . . 5
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
68 | 63, 67 | sylibr 223 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴) |
69 | | prex 4836 |
. . . . 5
⊢
{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V |
70 | 7, 6 | elsymgbas2 17624 |
. . . . 5
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V → ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴)) |
71 | 69, 70 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴) |
72 | 68, 71 | sylibr 223 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵) |
73 | | f1oprswap 6092 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
74 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
75 | 74, 65, 65 | f1oeq123d 6046 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → ({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
76 | 8, 75 | ax-mp 5 |
. . . . . 6
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
77 | 73, 76 | sylibr 223 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
78 | 77 | adantl 481 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
79 | | prex 4836 |
. . . . 5
⊢
{〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V |
80 | 7, 6 | elsymgbas2 17624 |
. . . . 5
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V → ({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴)) |
81 | 79, 80 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
82 | 78, 81 | sylibr 223 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵) |
83 | | opex 4859 |
. . . . . 6
⊢
〈𝐼, 𝐼〉 ∈ V |
84 | 83, 26 | pm3.2i 470 |
. . . . 5
⊢
(〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) |
85 | | opex 4859 |
. . . . . 6
⊢
〈𝐼, 𝐽〉 ∈ V |
86 | | opex 4859 |
. . . . . 6
⊢
〈𝐽, 𝐼〉 ∈ V |
87 | 85, 86 | pm3.2i 470 |
. . . . 5
⊢
(〈𝐼, 𝐽〉 ∈ V ∧
〈𝐽, 𝐼〉 ∈ V) |
88 | 84, 87 | pm3.2i 470 |
. . . 4
⊢
((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) |
89 | | opthg2 4874 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 ↔ (𝐼 = 𝐼 ∧ 𝐼 = 𝐽))) |
90 | | eqtr 2629 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐼 ∧ 𝐼 = 𝐽) → 𝐼 = 𝐽) |
91 | 89, 90 | syl6bi 242 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 → 𝐼 = 𝐽)) |
92 | 91 | necon3d 2803 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
93 | 92 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
94 | 45, 93 | sylbir 224 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
95 | 94 | imp 444 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉) |
96 | 54 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
97 | | opthg 4872 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
98 | 96, 97 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
99 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐽 ∧ 𝐼 = 𝐼) → 𝐼 = 𝐽) |
100 | 98, 99 | syl6bi 242 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 → 𝐼 = 𝐽)) |
101 | 100 | necon3d 2803 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
102 | 101 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
103 | 45, 102 | sylbir 224 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
104 | 103 | imp 444 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) |
105 | 95, 104 | jca 553 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
106 | 105 | orcd 406 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉))) |
107 | | prneimg 4328 |
. . . 4
⊢
(((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) → (((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) |
108 | 88, 106, 107 | mpsyl 66 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
109 | | hash2prd 13114 |
. . . 4
⊢ ((𝐵 ∈ V ∧ (#‘𝐵) = 2) → (({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}})) |
110 | 109 | imp 444 |
. . 3
⊢ (((𝐵 ∈ V ∧ (#‘𝐵) = 2) ∧ ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
111 | 44, 52, 72, 82, 108, 110 | syl23anc 1325 |
. 2
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
112 | 41, 111 | pm2.61ian 827 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |