| Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > usgrexmpl12ngrlic | Structured version Visualization version GIF version | ||
| Description: The graphs 𝐻 and 𝐺 are not locally isomorphic (𝐻 contains a triangle, see usgrexmpl1tri 47957, whereas 𝐺 does not, see usgrexmpl2trifr 47969. (Contributed by AV, 24-Aug-2025.) |
| Ref | Expression |
|---|---|
| usgrexmpl2.v | ⊢ 𝑉 = (0...5) |
| usgrexmpl2.e | ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
| usgrexmpl2.g | ⊢ 𝐺 = 〈𝑉, 𝐸〉 |
| usgrexmpl1.k | ⊢ 𝐾 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 |
| usgrexmpl1.h | ⊢ 𝐻 = 〈𝑉, 𝐾〉 |
| Ref | Expression |
|---|---|
| usgrexmpl12ngrlic | ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | usgrexmpl2.v | . . . . 5 ⊢ 𝑉 = (0...5) | |
| 2 | usgrexmpl2.e | . . . . 5 ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 | |
| 3 | usgrexmpl2.g | . . . . 5 ⊢ 𝐺 = 〈𝑉, 𝐸〉 | |
| 4 | 1, 2, 3 | usgrexmpl2 47959 | . . . 4 ⊢ 𝐺 ∈ USGraph |
| 5 | usgruhgr 29193 | . . . 4 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph) | |
| 6 | grlicsym 47946 | . . . 4 ⊢ (𝐺 ∈ UHGraph → (𝐺 ≃𝑙𝑔𝑟 𝐻 → 𝐻 ≃𝑙𝑔𝑟 𝐺)) | |
| 7 | 4, 5, 6 | mp2b 10 | . . 3 ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → 𝐻 ≃𝑙𝑔𝑟 𝐺) |
| 8 | usgrexmpl1.k | . . . 4 ⊢ 𝐾 = 〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 | |
| 9 | usgrexmpl1.h | . . . 4 ⊢ 𝐻 = 〈𝑉, 𝐾〉 | |
| 10 | 1, 8, 9 | usgrexmpl1tri 47957 | . . 3 ⊢ {0, 1, 2} ∈ (GrTriangles‘𝐻) |
| 11 | brgrlic 47937 | . . . . 5 ⊢ (𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ (𝐻 GraphLocIso 𝐺) ≠ ∅) | |
| 12 | n0 4352 | . . . . 5 ⊢ ((𝐻 GraphLocIso 𝐺) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐻 GraphLocIso 𝐺)) | |
| 13 | 11, 12 | bitri 275 | . . . 4 ⊢ (𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ ∃𝑓 𝑓 ∈ (𝐻 GraphLocIso 𝐺)) |
| 14 | 1, 2, 3 | usgrexmpl2trifr 47969 | . . . . . 6 ⊢ ¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) |
| 15 | 1, 8, 9 | usgrexmpl1 47954 | . . . . . . . . 9 ⊢ 𝐻 ∈ USGraph |
| 16 | usgruspgr 29187 | . . . . . . . . 9 ⊢ (𝐻 ∈ USGraph → 𝐻 ∈ USPGraph) | |
| 17 | 15, 16 | mp1i 13 | . . . . . . . 8 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → 𝐻 ∈ USPGraph) |
| 18 | usgruspgr 29187 | . . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ USPGraph) | |
| 19 | 4, 18 | mp1i 13 | . . . . . . . 8 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → 𝐺 ∈ USPGraph) |
| 20 | simpl 482 | . . . . . . . 8 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → 𝑓 ∈ (𝐻 GraphLocIso 𝐺)) | |
| 21 | simpr 484 | . . . . . . . 8 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → {0, 1, 2} ∈ (GrTriangles‘𝐻)) | |
| 22 | 17, 19, 20, 21 | grlimgrtri 47936 | . . . . . . 7 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺)) |
| 23 | 22 | ex 412 | . . . . . 6 ⊢ (𝑓 ∈ (𝐻 GraphLocIso 𝐺) → ({0, 1, 2} ∈ (GrTriangles‘𝐻) → ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺))) |
| 24 | pm2.21 123 | . . . . . 6 ⊢ (¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻)) | |
| 25 | 14, 23, 24 | mpsylsyld 69 | . . . . 5 ⊢ (𝑓 ∈ (𝐻 GraphLocIso 𝐺) → ({0, 1, 2} ∈ (GrTriangles‘𝐻) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻)) |
| 26 | 25 | exlimiv 1930 | . . . 4 ⊢ (∃𝑓 𝑓 ∈ (𝐻 GraphLocIso 𝐺) → ({0, 1, 2} ∈ (GrTriangles‘𝐻) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻)) |
| 27 | 13, 26 | sylbi 217 | . . 3 ⊢ (𝐻 ≃𝑙𝑔𝑟 𝐺 → ({0, 1, 2} ∈ (GrTriangles‘𝐻) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻)) |
| 28 | 7, 10, 27 | mpisyl 21 | . 2 ⊢ (𝐺 ≃𝑙𝑔𝑟 𝐻 → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻) |
| 29 | 28 | pm2.01i 189 | 1 ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∃wex 1779 ∈ wcel 2108 ≠ wne 2939 ∅c0 4332 {cpr 4626 {ctp 4628 〈cop 4630 class class class wbr 5141 ‘cfv 6559 (class class class)co 7429 0cc0 11151 1c1 11152 2c2 12317 3c3 12318 4c4 12319 5c5 12320 ...cfz 13543 〈“cs7 14881 UHGraphcuhgr 29063 USPGraphcuspgr 29155 USGraphcusgr 29156 GrTrianglescgrtri 47877 GraphLocIso cgrlim 47916 ≃𝑙𝑔𝑟 cgrlic 47917 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5277 ax-sep 5294 ax-nul 5304 ax-pow 5363 ax-pr 5430 ax-un 7751 ax-cnex 11207 ax-resscn 11208 ax-1cn 11209 ax-icn 11210 ax-addcl 11211 ax-addrcl 11212 ax-mulcl 11213 ax-mulrcl 11214 ax-mulcom 11215 ax-addass 11216 ax-mulass 11217 ax-distr 11218 ax-i2m1 11219 ax-1ne0 11220 ax-1rid 11221 ax-rnegex 11222 ax-rrecex 11223 ax-cnre 11224 ax-pre-lttri 11225 ax-pre-lttrn 11226 ax-pre-ltadd 11227 ax-pre-mulgt0 11228 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4906 df-int 4945 df-iun 4991 df-br 5142 df-opab 5204 df-mpt 5224 df-tr 5258 df-id 5576 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5635 df-we 5637 df-xp 5689 df-rel 5690 df-cnv 5691 df-co 5692 df-dm 5693 df-rn 5694 df-res 5695 df-ima 5696 df-pred 6319 df-ord 6385 df-on 6386 df-lim 6387 df-suc 6388 df-iota 6512 df-fun 6561 df-fn 6562 df-f 6563 df-f1 6564 df-fo 6565 df-f1o 6566 df-fv 6567 df-riota 7386 df-ov 7432 df-oprab 7433 df-mpo 7434 df-om 7884 df-1st 8010 df-2nd 8011 df-frecs 8302 df-wrecs 8333 df-recs 8407 df-rdg 8446 df-1o 8502 df-2o 8503 df-3o 8504 df-oadd 8506 df-er 8741 df-map 8864 df-en 8982 df-dom 8983 df-sdom 8984 df-fin 8985 df-dju 9937 df-card 9975 df-pnf 11293 df-mnf 11294 df-xr 11295 df-ltxr 11296 df-le 11297 df-sub 11490 df-neg 11491 df-nn 12263 df-2 12325 df-3 12326 df-4 12327 df-5 12328 df-6 12329 df-7 12330 df-n0 12523 df-xnn0 12596 df-z 12610 df-uz 12875 df-fz 13544 df-fzo 13691 df-hash 14366 df-word 14549 df-concat 14605 df-s1 14630 df-s2 14883 df-s3 14884 df-s4 14885 df-s5 14886 df-s6 14887 df-s7 14888 df-vtx 29005 df-iedg 29006 df-edg 29055 df-uhgr 29065 df-upgr 29089 df-umgr 29090 df-uspgr 29157 df-usgr 29158 df-nbgr 29340 df-clnbgr 47779 df-isubgr 47820 df-grim 47837 df-gric 47840 df-grtri 47878 df-grlim 47918 df-grlic 47921 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |