Metamath Proof Explorer

Theorem usgrexmpl12ngrlic

Description: The graphs H and G are not locally isomorphic ( H contains a triangle, see usgrexmpl1tri , whereas G does not, see usgrexmpl2trifr . (Contributed by AV, 24-Aug-2025)

Ref Expression
Hypotheses 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 ⊢ 𝐻 = ⟨ 𝑉 , 𝐾 ⟩
Assertion usgrexmpl12ngrlic ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 usgrexmpl1.k ⊢ 𝐾 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
5 usgrexmpl1.h ⊢ 𝐻 = ⟨ 𝑉 , 𝐾 ⟩
6 1 2 3 usgrexmpl2 ⊢ 𝐺 ∈ USGraph
7 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
8 grlicsym ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → 𝐻 ≃𝑙𝑔𝑟 𝐺 ) )
9 6 7 8 mp2b ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → 𝐻 ≃𝑙𝑔𝑟 𝐺 )
10 1 4 5 usgrexmpl1tri ⊢ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 )
11 brgrlic ⊢ ( 𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ ( 𝐻 GraphLocIso 𝐺 ) ≠ ∅ )
12 n0 ⊢ ( ( 𝐻 GraphLocIso 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) )
13 11 12 bitri ⊢ ( 𝐻 ≃𝑙𝑔𝑟 𝐺 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) )
14 1 2 3 usgrexmpl2trifr ⊢ ¬ ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 )
15 1 4 5 usgrexmpl1 ⊢ 𝐻 ∈ USGraph
16 usgruspgr ⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ USPGraph )
17 15 16 mp1i ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝐻 ∈ USPGraph )
18 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
19 6 18 mp1i ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝐺 ∈ USPGraph )
20 simpl ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) )
21 simpr ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) )
22 17 19 20 21 grlimgrtri ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) )
23 22 ex ⊢ ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ) )
24 pm2.21 ⊢ ( ¬ ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
25 14 23 24 mpsylsyld ⊢ ( 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
26 25 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphLocIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
27 13 26 sylbi ⊢ ( 𝐻 ≃𝑙𝑔𝑟 𝐺 → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 ) )
28 9 10 27 mpisyl ⊢ ( 𝐺 ≃𝑙𝑔𝑟 𝐻 → ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻 )
29 28 pm2.01i ⊢ ¬ 𝐺 ≃𝑙𝑔𝑟 𝐻