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	$⊢ V = (0 \dots 5)$
	usgrexmpl2.e	$⊢ E = ⟨“ \{0, 1\} \{1, 2\} \{2, 3\} \{3, 4\} \{4, 5\} \{0, 3\} \{0, 5\} ”⟩$
	usgrexmpl2.g	$⊢ G = ⟨V, E⟩$
	usgrexmpl1.k	$⊢ K = ⟨“ \{0, 1\} \{0, 2\} \{1, 2\} \{0, 3\} \{3, 4\} \{3, 5\} \{4, 5\} ”⟩$
	usgrexmpl1.h	$⊢ H = ⟨V, K⟩$
Assertion	usgrexmpl12ngric	$⊢ \neg G ≃_{𝑔𝑟} H$

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl2.v	$⊢ V = (0 \dots 5)$
2		usgrexmpl2.e	$⊢ E = ⟨“ \{0, 1\} \{1, 2\} \{2, 3\} \{3, 4\} \{4, 5\} \{0, 3\} \{0, 5\} ”⟩$
3		usgrexmpl2.g	$⊢ G = ⟨V, E⟩$
4		usgrexmpl1.k	$⊢ K = ⟨“ \{0, 1\} \{0, 2\} \{1, 2\} \{0, 3\} \{3, 4\} \{3, 5\} \{4, 5\} ”⟩$
5		usgrexmpl1.h	$⊢ H = ⟨V, K⟩$
6	1 2 3	usgrexmpl2	$⊢ G \in USGraph$
7		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
8	6 7	ax-mp	$⊢ G \in UHGraph$
9		gricsym	$⊢ G \in UHGraph \to (G ≃_{𝑔𝑟} H \to H ≃_{𝑔𝑟} G)$
10	8 9	ax-mp	$⊢ G ≃_{𝑔𝑟} H \to H ≃_{𝑔𝑟} G$
11	1 4 5	usgrexmpl1tri	Could not format { 0 , 1 , 2 } e. ( GrTriangles ` H ) : No typesetting found for \|- { 0 , 1 , 2 } e. ( GrTriangles ` H ) with typecode \|-
12		brgric	$⊢ H ≃_{𝑔𝑟} G \leftrightarrow H GraphIso G \neq \emptyset$
13		n0	$⊢ H GraphIso G \neq \emptyset \leftrightarrow \exists f f \in (H GraphIso G)$
14	12 13	bitri	$⊢ H ≃_{𝑔𝑟} G \leftrightarrow \exists f f \in (H GraphIso G)$
15	1 2 3	usgrexmpl2trifr	Could not format -. E. t t e. ( GrTriangles ` G ) : No typesetting found for \|- -. E. t t e. ( GrTriangles ` G ) with typecode \|-
16	1 4 5	usgrexmpl1	$⊢ H \in USGraph$
17		usgruhgr	$⊢ H \in USGraph \to H \in UHGraph$
18	16 17	ax-mp	$⊢ H \in UHGraph$
19	18	a1i	Could not format ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. UHGraph ) : No typesetting found for \|- ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. UHGraph ) with typecode \|-
20	8	a1i	Could not format ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. UHGraph ) : No typesetting found for \|- ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. UHGraph ) with typecode \|-
21		simpl	Could not format ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphIso G ) ) : No typesetting found for \|- ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphIso G ) ) with typecode \|-
22		simpr	Could not format ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) : No typesetting found for \|- ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) with typecode \|-
23	19 20 21 22	grimgrtri	Could not format ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( ( f e. ( H GraphIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) with typecode \|-
24	23	ex	Could not format ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) with typecode \|-
25		alnex	Could not format ( A. t -. t e. ( GrTriangles ` G ) <-> -. E. t t e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( A. t -. t e. ( GrTriangles ` G ) <-> -. E. t t e. ( GrTriangles ` G ) ) with typecode \|-
26		vex	$⊢ f \in V$
27	26	imaex	$⊢ f [\{0, 1, 2\}] \in V$
28		id	$⊢ f [\{0, 1, 2\}] \in V \to f [\{0, 1, 2\}] \in V$
29		eleq1	Could not format ( t = ( f " { 0 , 1 , 2 } ) -> ( t e. ( GrTriangles ` G ) <-> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( t = ( f " { 0 , 1 , 2 } ) -> ( t e. ( GrTriangles ` G ) <-> ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) with typecode \|-
30	29	notbid	Could not format ( t = ( f " { 0 , 1 , 2 } ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( t = ( f " { 0 , 1 , 2 } ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) with typecode \|-
31	30	adantl	Could not format ( ( ( f " { 0 , 1 , 2 } ) e. _V /\ t = ( f " { 0 , 1 , 2 } ) ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( ( ( f " { 0 , 1 , 2 } ) e. _V /\ t = ( f " { 0 , 1 , 2 } ) ) -> ( -. t e. ( GrTriangles ` G ) <-> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) with typecode \|-
32	28 31	spcdv	Could not format ( ( f " { 0 , 1 , 2 } ) e. _V -> ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( ( f " { 0 , 1 , 2 } ) e. _V -> ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) ) with typecode \|-
33	27 32	ax-mp	Could not format ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( A. t -. t e. ( GrTriangles ` G ) -> -. ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) ) with typecode \|-
34	33	pm2.21d	Could not format ( A. t -. t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) ) : No typesetting found for \|- ( A. t -. t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) ) with typecode \|-
35	25 34	sylbir	Could not format ( -. E. t t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) ) : No typesetting found for \|- ( -. E. t t e. ( GrTriangles ` G ) -> ( ( f " { 0 , 1 , 2 } ) e. ( GrTriangles ` G ) -> -. G ~=gr H ) ) with typecode \|-
36	15 24 35	mpsylsyld	Could not format ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) : No typesetting found for \|- ( f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) with typecode \|-
37	36	exlimiv	Could not format ( E. f f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) : No typesetting found for \|- ( E. f f e. ( H GraphIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) with typecode \|-
38	14 37	sylbi	Could not format ( H ~=gr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) : No typesetting found for \|- ( H ~=gr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=gr H ) ) with typecode \|-
39	10 11 38	mpisyl	$⊢ G ≃_{𝑔𝑟} H \to \neg G ≃_{𝑔𝑟} H$
40	39	pm2.01i	$⊢ \neg G ≃_{𝑔𝑟} H$

Metamath Proof Explorer

Theorem usgrexmpl12ngric

Proof