Proof of Theorem symg2bas
| 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 19408 |
. . . 4
⊢ (𝐽 ∈ 𝑊 → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
| 5 | 4 | ad2antll 729 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘(SymGrp‘{𝐽})) = {{〈𝐽, 𝐽〉}}) |
| 6 | | symg1bas.2 |
. . . 4
⊢ 𝐵 = (Base‘𝐺) |
| 7 | | symg1bas.1 |
. . . . . 6
⊢ 𝐺 = (SymGrp‘𝐴) |
| 8 | | symg2bas.0 |
. . . . . . . 8
⊢ 𝐴 = {𝐼, 𝐽} |
| 9 | | df-pr 4629 |
. . . . . . . . 9
⊢ {𝐼, 𝐽} = ({𝐼} ∪ {𝐽}) |
| 10 | | sneq 4636 |
. . . . . . . . . . . 12
⊢ (𝐼 = 𝐽 → {𝐼} = {𝐽}) |
| 11 | 10 | uneq1d 4167 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝐽 → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
| 12 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = ({𝐽} ∪ {𝐽})) |
| 13 | | unidm 4157 |
. . . . . . . . . 10
⊢ ({𝐽} ∪ {𝐽}) = {𝐽} |
| 14 | 12, 13 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ({𝐼} ∪ {𝐽}) = {𝐽}) |
| 15 | 9, 14 | eqtrid 2789 |
. . . . . . . 8
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {𝐼, 𝐽} = {𝐽}) |
| 16 | 8, 15 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐴 = {𝐽}) |
| 17 | 16 | fveq2d 6910 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (SymGrp‘𝐴) = (SymGrp‘{𝐽})) |
| 18 | 7, 17 | eqtrid 2789 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐺 = (SymGrp‘{𝐽})) |
| 19 | 18 | fveq2d 6910 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (Base‘𝐺) = (Base‘(SymGrp‘{𝐽}))) |
| 20 | 6, 19 | eqtrid 2789 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = (Base‘(SymGrp‘{𝐽}))) |
| 21 | | id 22 |
. . . . . . . . 9
⊢ (𝐼 = 𝐽 → 𝐼 = 𝐽) |
| 22 | 21, 21 | opeq12d 4881 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
| 23 | 22 | adantr 480 |
. . . . . . 7
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 = 〈𝐽, 𝐽〉) |
| 24 | 23 | preq1d 4739 |
. . . . . 6
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
| 25 | | eqid 2737 |
. . . . . . 7
⊢
〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 |
| 26 | | opex 5469 |
. . . . . . . 8
⊢
〈𝐽, 𝐽〉 ∈ V |
| 27 | 26, 26 | preqsn 4862 |
. . . . . . 7
⊢
({〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ↔ (〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉 ∧ 〈𝐽, 𝐽〉 = 〈𝐽, 𝐽〉)) |
| 28 | 25, 25, 27 | mpbir2an 711 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
| 29 | 24, 28 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉}) |
| 30 | | opeq1 4873 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐼, 𝐽〉 = 〈𝐽, 𝐽〉) |
| 31 | | opeq2 4874 |
. . . . . . . 8
⊢ (𝐼 = 𝐽 → 〈𝐽, 𝐼〉 = 〈𝐽, 𝐽〉) |
| 32 | 30, 31 | preq12d 4741 |
. . . . . . 7
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉, 〈𝐽, 𝐽〉}) |
| 33 | 32, 28 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐼 = 𝐽 → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
| 34 | 33 | adantr 480 |
. . . . 5
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐽, 𝐽〉}) |
| 35 | 29, 34 | preq12d 4741 |
. . . 4
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}}) |
| 36 | | eqid 2737 |
. . . . 5
⊢
{〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} |
| 37 | | snex 5436 |
. . . . . 6
⊢
{〈𝐽, 𝐽〉} ∈
V |
| 38 | 37, 37 | preqsn 4862 |
. . . . 5
⊢
({{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} ↔ ({〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉} ∧ {〈𝐽, 𝐽〉} = {〈𝐽, 𝐽〉})) |
| 39 | 36, 36, 38 | mpbir2an 711 |
. . . 4
⊢
{{〈𝐽, 𝐽〉}, {〈𝐽, 𝐽〉}} = {{〈𝐽, 𝐽〉}} |
| 40 | 35, 39 | eqtrdi 2793 |
. . 3
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}} = {{〈𝐽, 𝐽〉}}) |
| 41 | 5, 20, 40 | 3eqtr4d 2787 |
. 2
⊢ ((𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
| 42 | 6 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 43 | 42 | a1i 11 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 ∈ V) |
| 44 | | neqne 2948 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → 𝐼 ≠ 𝐽) |
| 45 | 44 | anim2i 617 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
| 46 | | df-3an 1089 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) ↔ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ 𝐼 ≠ 𝐽)) |
| 47 | 45, 46 | sylibr 234 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) ∧ ¬ 𝐼 = 𝐽) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
| 48 | 47 | ancoms 458 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽)) |
| 49 | 7, 6, 8 | symg2hash 19409 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2) |
| 50 | 48, 49 | syl 17 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (♯‘𝐵) = 2) |
| 51 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐼 ∈ 𝑉) |
| 52 | 51 | ancri 549 |
. . . . . . 7
⊢ (𝐼 ∈ 𝑉 → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
| 53 | | id 22 |
. . . . . . . 8
⊢ (𝐽 ∈ 𝑊 → 𝐽 ∈ 𝑊) |
| 54 | 53 | ancri 549 |
. . . . . . 7
⊢ (𝐽 ∈ 𝑊 → (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) |
| 55 | 52, 54 | anim12i 613 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊))) |
| 56 | | df-ne 2941 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 ↔ ¬ 𝐼 = 𝐽) |
| 57 | | id 22 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → 𝐼 ≠ 𝐽) |
| 58 | 57 | ancri 549 |
. . . . . . 7
⊢ (𝐼 ≠ 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
| 59 | 56, 58 | sylbir 235 |
. . . . . 6
⊢ (¬
𝐼 = 𝐽 → (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) |
| 60 | | f1oprg 6893 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) → ((𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
| 61 | 60 | imp 406 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) ∧ (𝐽 ∈ 𝑊 ∧ 𝐽 ∈ 𝑊)) ∧ (𝐼 ≠ 𝐽 ∧ 𝐼 ≠ 𝐽)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
| 62 | 55, 59, 61 | syl2anr 597 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
| 63 | | eqidd 2738 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} = {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}) |
| 64 | | id 22 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → 𝐴 = {𝐼, 𝐽}) |
| 65 | 63, 64, 64 | f1oeq123d 6842 |
. . . . . 6
⊢ (𝐴 = {𝐼, 𝐽} → ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
| 66 | 8, 65 | ax-mp 5 |
. . . . 5
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
| 67 | 62, 66 | sylibr 234 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴) |
| 68 | | prex 5437 |
. . . . 5
⊢
{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V |
| 69 | 7, 6 | elsymgbas2 19390 |
. . . . 5
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ V → ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴)) |
| 70 | 68, 69 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ↔ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}:𝐴–1-1-onto→𝐴) |
| 71 | 67, 70 | sylibr 234 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵) |
| 72 | | f1oprswap 6892 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
| 73 | | eqidd 2738 |
. . . . . . . 8
⊢ (𝐴 = {𝐼, 𝐽} → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} = {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
| 74 | 73, 64, 64 | f1oeq123d 6842 |
. . . . . . 7
⊢ (𝐴 = {𝐼, 𝐽} → ({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽})) |
| 75 | 8, 74 | ax-mp 5 |
. . . . . 6
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:{𝐼, 𝐽}–1-1-onto→{𝐼, 𝐽}) |
| 76 | 72, 75 | sylibr 234 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
| 77 | 76 | adantl 481 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
| 78 | | prex 5437 |
. . . . 5
⊢
{〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V |
| 79 | 7, 6 | elsymgbas2 19390 |
. . . . 5
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ V → ({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴)) |
| 80 | 78, 79 | ax-mp 5 |
. . . 4
⊢
({〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ↔ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}:𝐴–1-1-onto→𝐴) |
| 81 | 77, 80 | sylibr 234 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵) |
| 82 | | opex 5469 |
. . . . . 6
⊢
〈𝐼, 𝐼〉 ∈ V |
| 83 | 82, 26 | pm3.2i 470 |
. . . . 5
⊢
(〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) |
| 84 | | opex 5469 |
. . . . . 6
⊢
〈𝐼, 𝐽〉 ∈ V |
| 85 | | opex 5469 |
. . . . . 6
⊢
〈𝐽, 𝐼〉 ∈ V |
| 86 | 84, 85 | pm3.2i 470 |
. . . . 5
⊢
(〈𝐼, 𝐽〉 ∈ V ∧
〈𝐽, 𝐼〉 ∈ V) |
| 87 | 83, 86 | pm3.2i 470 |
. . . 4
⊢
((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) |
| 88 | | opthg2 5484 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 ↔ (𝐼 = 𝐼 ∧ 𝐼 = 𝐽))) |
| 89 | | eqtr 2760 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐼 ∧ 𝐼 = 𝐽) → 𝐼 = 𝐽) |
| 90 | 88, 89 | biimtrdi 253 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐼, 𝐽〉 → 𝐼 = 𝐽)) |
| 91 | 90 | necon3d 2961 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
| 92 | 91 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
| 93 | 56, 92 | sylbir 235 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉)) |
| 94 | 93 | imp 406 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉) |
| 95 | 52 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉)) |
| 96 | | opthg 5482 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐼 ∈ 𝑉) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
| 97 | 95, 96 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 ↔ (𝐼 = 𝐽 ∧ 𝐼 = 𝐼))) |
| 98 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝐼 = 𝐽 ∧ 𝐼 = 𝐼) → 𝐼 = 𝐽) |
| 99 | 97, 98 | biimtrdi 253 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (〈𝐼, 𝐼〉 = 〈𝐽, 𝐼〉 → 𝐼 = 𝐽)) |
| 100 | 99 | necon3d 2961 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 ≠ 𝐽 → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
| 101 | 100 | com12 32 |
. . . . . . . 8
⊢ (𝐼 ≠ 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
| 102 | 56, 101 | sylbir 235 |
. . . . . . 7
⊢ (¬
𝐼 = 𝐽 → ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
| 103 | 102 | imp 406 |
. . . . . 6
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) |
| 104 | 94, 103 | jca 511 |
. . . . 5
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → (〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉)) |
| 105 | 104 | orcd 874 |
. . . 4
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → ((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉))) |
| 106 | | prneimg 4854 |
. . . 4
⊢
(((〈𝐼, 𝐼〉 ∈ V ∧
〈𝐽, 𝐽〉 ∈ V) ∧ (〈𝐼, 𝐽〉 ∈ V ∧ 〈𝐽, 𝐼〉 ∈ V)) → (((〈𝐼, 𝐼〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐼, 𝐼〉 ≠ 〈𝐽, 𝐼〉) ∨ (〈𝐽, 𝐽〉 ≠ 〈𝐼, 𝐽〉 ∧ 〈𝐽, 𝐽〉 ≠ 〈𝐽, 𝐼〉)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) |
| 107 | 87, 105, 106 | mpsyl 68 |
. . 3
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) |
| 108 | | hash2prd 14514 |
. . . 4
⊢ ((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
→ (({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}})) |
| 109 | 108 | imp 406 |
. . 3
⊢ (((𝐵 ∈ V ∧
(♯‘𝐵) = 2)
∧ ({〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ∈ 𝐵 ∧ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉} ∈ 𝐵 ∧ {〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉} ≠ {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉})) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
| 110 | 43, 50, 71, 81, 107, 109 | syl23anc 1379 |
. 2
⊢ ((¬
𝐼 = 𝐽 ∧ (𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊)) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |
| 111 | 41, 110 | pm2.61ian 812 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) |