![]() |
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 47841, whereas 𝐺 does not, see usgrexmpl2trifr 47853. (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 47843 | . . . 4 ⊢ 𝐺 ∈ USGraph |
5 | usgruhgr 29199 | . . . 4 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph) | |
6 | grlicsym 47831 | . . . 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 47841 | . . 3 ⊢ {0, 1, 2} ∈ (GrTriangles‘𝐻) |
11 | brgrlic 47822 | . . . . 5 ⊢ (𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ (𝐻 GraphLocIso 𝐺) ≠ ∅) | |
12 | n0 4359 | . . . . 5 ⊢ ((𝐻 GraphLocIso 𝐺) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ (𝐻 GraphLocIso 𝐺)) | |
13 | 11, 12 | bitri 275 | . . . 4 ⊢ (𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ ∃𝑓 𝑓 ∈ (𝐻 GraphLocIso 𝐺)) |
14 | 1, 2, 3 | usgrexmpl2trifr 47853 | . . . . . 6 ⊢ ¬ ∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) |
15 | 1, 8, 9 | usgrexmpl1 47838 | . . . . . . . . 9 ⊢ 𝐻 ∈ USGraph |
16 | usgruspgr 29193 | . . . . . . . . 9 ⊢ (𝐻 ∈ USGraph → 𝐻 ∈ USPGraph) | |
17 | 15, 16 | mp1i 13 | . . . . . . . 8 ⊢ ((𝑓 ∈ (𝐻 GraphLocIso 𝐺) ∧ {0, 1, 2} ∈ (GrTriangles‘𝐻)) → 𝐻 ∈ USPGraph) |
18 | usgruspgr 29193 | . . . . . . . . 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 47821 | . . . . . . 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 1926 | . . . 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 1535 ∃wex 1774 ∈ wcel 2104 ≠ wne 2936 ∅c0 4339 {cpr 4632 {ctp 4634 〈cop 4636 class class class wbr 5149 ‘cfv 6558 (class class class)co 7425 0cc0 11146 1c1 11147 2c2 12312 3c3 12313 4c4 12314 5c5 12315 ...cfz 13537 〈“cs7 14871 UHGraphcuhgr 29069 USPGraphcuspgr 29161 USGraphcusgr 29162 GrTrianglescgrtri 47789 GraphLocIso cgrlim 47801 ≃𝑙𝑔𝑟 cgrlic 47802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1963 ax-7 2003 ax-8 2106 ax-9 2114 ax-10 2137 ax-11 2153 ax-12 2173 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5366 ax-pr 5430 ax-un 7747 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1538 df-fal 1548 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2536 df-eu 2565 df-clab 2711 df-cleq 2725 df-clel 2812 df-nfc 2888 df-ne 2937 df-nel 3043 df-ral 3058 df-rex 3067 df-reu 3377 df-rab 3433 df-v 3479 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-tp 4635 df-op 4637 df-uni 4915 df-int 4954 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 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 6317 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6510 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7381 df-ov 7428 df-oprab 7429 df-mpo 7430 df-om 7881 df-1st 8007 df-2nd 8008 df-frecs 8299 df-wrecs 8330 df-recs 8404 df-rdg 8443 df-1o 8499 df-2o 8500 df-3o 8501 df-oadd 8503 df-er 8738 df-map 8861 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-dju 9932 df-card 9970 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11485 df-neg 11486 df-nn 12258 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-n0 12518 df-xnn0 12591 df-z 12605 df-uz 12870 df-fz 13538 df-fzo 13682 df-hash 14356 df-word 14539 df-concat 14595 df-s1 14620 df-s2 14873 df-s3 14874 df-s4 14875 df-s5 14876 df-s6 14877 df-s7 14878 df-vtx 29011 df-iedg 29012 df-edg 29061 df-uhgr 29071 df-upgr 29095 df-umgr 29096 df-uspgr 29163 df-usgr 29164 df-nbgr 29346 df-clnbgr 47694 df-isubgr 47734 df-grim 47749 df-gric 47752 df-grtri 47790 df-grlim 47803 df-grlic 47806 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |