Metamath Proof Explorer

Theorem usgrexmpl12ngric

Description: The graphs H and G are not isomorphic ( H contains a triangle, see usgrexmpl1tri , whereas G does not, see usgrexmpl2trifr . (Contributed by AV, 10-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 usgrexmpl12ngric ¬ 𝐺 ≃𝑔𝑟 𝐻

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 6 7 ax-mp ⊢ 𝐺 ∈ UHGraph
9 gricsym ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ≃𝑔𝑟 𝐻 → 𝐻 ≃𝑔𝑟 𝐺 ) )
10 8 9 ax-mp ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 → 𝐻 ≃𝑔𝑟 𝐺 )
11 1 4 5 usgrexmpl1tri ⊢ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 )
12 brgric ⊢ ( 𝐻 ≃𝑔𝑟 𝐺 ↔ ( 𝐻 GraphIso 𝐺 ) ≠ ∅ )
13 n0 ⊢ ( ( 𝐻 GraphIso 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) )
14 12 13 bitri ⊢ ( 𝐻 ≃𝑔𝑟 𝐺 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) )
15 1 2 3 usgrexmpl2trifr ⊢ ¬ ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 )
16 1 4 5 usgrexmpl1 ⊢ 𝐻 ∈ USGraph
17 usgruhgr ⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ UHGraph )
18 16 17 ax-mp ⊢ 𝐻 ∈ UHGraph
19 18 a1i ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝐻 ∈ UHGraph )
20 8 a1i ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝐺 ∈ UHGraph )
21 simpl ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) )
22 simpr ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) )
23 19 20 21 22 grimgrtri ⊢ ( ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) ∧ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) ) → ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) )
24 23 ex ⊢ ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) ) )
25 alnex ⊢ ( ∀ 𝑡 ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ¬ ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) )
26 vex ⊢ 𝑓 ∈ V
27 26 imaex ⊢ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ V
28 id ⊢ ( ( 𝑓 “ { 0 , 1 , 2 } ) ∈ V → ( 𝑓 “ { 0 , 1 , 2 } ) ∈ V )
29 eleq1 ⊢ ( 𝑡 = ( 𝑓 “ { 0 , 1 , 2 } ) → ( 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) ) )
30 29 notbid ⊢ ( 𝑡 = ( 𝑓 “ { 0 , 1 , 2 } ) → ( ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ¬ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) ) )
31 30 adantl ⊢ ( ( ( 𝑓 “ { 0 , 1 , 2 } ) ∈ V ∧ 𝑡 = ( 𝑓 “ { 0 , 1 , 2 } ) ) → ( ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ¬ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) ) )
32 28 31 spcdv ⊢ ( ( 𝑓 “ { 0 , 1 , 2 } ) ∈ V → ( ∀ 𝑡 ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ¬ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) ) )
33 27 32 ax-mp ⊢ ( ∀ 𝑡 ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ¬ ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) )
34 33 pm2.21d ⊢ ( ∀ 𝑡 ¬ 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ( ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
35 25 34 sylbir ⊢ ( ¬ ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) → ( ( 𝑓 “ { 0 , 1 , 2 } ) ∈ ( GrTriangles ‘ 𝐺 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
36 15 24 35 mpsylsyld ⊢ ( 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
37 36 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐻 GraphIso 𝐺 ) → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
38 14 37 sylbi ⊢ ( 𝐻 ≃𝑔𝑟 𝐺 → ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐻 ) → ¬ 𝐺 ≃𝑔𝑟 𝐻 ) )
39 10 11 38 mpisyl ⊢ ( 𝐺 ≃𝑔𝑟 𝐻 → ¬ 𝐺 ≃𝑔𝑟 𝐻 )
40 39 pm2.01i ⊢ ¬ 𝐺 ≃𝑔𝑟 𝐻