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	$⊢ 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	usgrexmpl12ngrlic	$⊢ \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		grlicsym	$⊢ G \in UHGraph \to (G ≃_{𝑙𝑔𝑟} H \to H ≃_{𝑙𝑔𝑟} G)$
9	6 7 8	mp2b	$⊢ G ≃_{𝑙𝑔𝑟} H \to H ≃_{𝑙𝑔𝑟} G$
10	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 \|-
11		brgrlic	$⊢ H ≃_{𝑙𝑔𝑟} G \leftrightarrow H GraphLocIso G \neq \emptyset$
12		n0	$⊢ H GraphLocIso G \neq \emptyset \leftrightarrow \exists f f \in (H GraphLocIso G)$
13	11 12	bitri	$⊢ H ≃_{𝑙𝑔𝑟} G \leftrightarrow \exists f f \in (H GraphLocIso G)$
14	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 \|-
15	1 4 5	usgrexmpl1	$⊢ H \in USGraph$
16		usgruspgr	$⊢ H \in USGraph \to H \in USHGraph$
17	15 16	mp1i	Could not format ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. USPGraph ) : No typesetting found for \|- ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> H e. USPGraph ) with typecode \|-
18		usgruspgr	$⊢ G \in USGraph \to G \in USHGraph$
19	6 18	mp1i	Could not format ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. USPGraph ) : No typesetting found for \|- ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> G e. USPGraph ) with typecode \|-
20		simpl	Could not format ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphLocIso G ) ) : No typesetting found for \|- ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> f e. ( H GraphLocIso G ) ) with typecode \|-
21		simpr	Could not format ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) : No typesetting found for \|- ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) with typecode \|-
22	17 19 20 21	grlimgrtri	Could not format ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> E. t t e. ( GrTriangles ` G ) ) : No typesetting found for \|- ( ( f e. ( H GraphLocIso G ) /\ { 0 , 1 , 2 } e. ( GrTriangles ` H ) ) -> E. t t e. ( GrTriangles ` G ) ) with typecode \|-
23	22	ex	Could not format ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> E. t t e. ( GrTriangles ` G ) ) ) : No typesetting found for \|- ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> E. t t e. ( GrTriangles ` G ) ) ) with typecode \|-
24		pm2.21	Could not format ( -. E. t t e. ( GrTriangles ` G ) -> ( E. t t e. ( GrTriangles ` G ) -> -. G ~=lgr H ) ) : No typesetting found for \|- ( -. E. t t e. ( GrTriangles ` G ) -> ( E. t t e. ( GrTriangles ` G ) -> -. G ~=lgr H ) ) with typecode \|-
25	14 23 24	mpsylsyld	Could not format ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) : No typesetting found for \|- ( f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) with typecode \|-
26	25	exlimiv	Could not format ( E. f f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) : No typesetting found for \|- ( E. f f e. ( H GraphLocIso G ) -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) with typecode \|-
27	13 26	sylbi	Could not format ( H ~=lgr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) : No typesetting found for \|- ( H ~=lgr G -> ( { 0 , 1 , 2 } e. ( GrTriangles ` H ) -> -. G ~=lgr H ) ) with typecode \|-
28	9 10 27	mpisyl	$⊢ G ≃_{𝑙𝑔𝑟} H \to \neg G ≃_{𝑙𝑔𝑟} H$
29	28	pm2.01i	$⊢ \neg G ≃_{𝑙𝑔𝑟} H$

Metamath Proof Explorer

Theorem usgrexmpl12ngrlic

Proof