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

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl2.v	$$⊢V=\left(0\dots 5\right)$$
2		usgrexmpl2.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{3,4\right\}\left\{4,5\right\}\left\{0,3\right\}\left\{0,5\right\}”⟩$$
3		usgrexmpl2.g	$$⊢G=⟨V,E⟩$$
4		usgrexmpl1.k	$$⊢K=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{1,2\right\}\left\{0,3\right\}\left\{3,4\right\}\left\{3,5\right\}\left\{4,5\right\}”⟩$$
5		usgrexmpl1.h	$$⊢H=⟨V,K⟩$$
6	1 2 3	usgrexmpl2	$$⊢G\in \mathrm{USGraph}$$
7		usgruhgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{UHGraph}$$
8		grlicsym	$$⊢G\in \mathrm{UHGraph}\to \left(G{\simeq }_{𝑙𝑔𝑟}H\to H{\simeq }_{𝑙𝑔𝑟}G\right)$$
9	6 7 8	mp2b	$$⊢G{\simeq }_{𝑙𝑔𝑟}H\to H{\simeq }_{𝑙𝑔𝑟}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{\simeq }_{𝑙𝑔𝑟}G\leftrightarrow H\mathrm{GraphLocIso}G\ne \varnothing$$
12		n0	$$⊢H\mathrm{GraphLocIso}G\ne \varnothing \leftrightarrow \exists ff\in \left(H\mathrm{GraphLocIso}G\right)$$
13	11 12	bitri	$$⊢H{\simeq }_{𝑙𝑔𝑟}G\leftrightarrow \exists ff\in \left(H\mathrm{GraphLocIso}G\right)$$
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 \mathrm{USGraph}$$
16		usgruspgr	$$⊢H\in \mathrm{USGraph}\to H\in \mathrm{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 \mathrm{USGraph}\to G\in \mathrm{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{\simeq }_{𝑙𝑔𝑟}H\to \neg G{\simeq }_{𝑙𝑔𝑟}H$$
29	28	pm2.01i	$$⊢\neg G{\simeq }_{𝑙𝑔𝑟}H$$