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	$$⊢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	usgrexmpl12ngric	$$⊢\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	6 7	ax-mp	$$⊢G\in \mathrm{UHGraph}$$
9		gricsym	$$⊢G\in \mathrm{UHGraph}\to \left(G{\simeq }_{𝑔𝑟}H\to H{\simeq }_{𝑔𝑟}G\right)$$
10	8 9	ax-mp	$$⊢G{\simeq }_{𝑔𝑟}H\to H{\simeq }_{𝑔𝑟}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{\simeq }_{𝑔𝑟}G\leftrightarrow H\mathrm{GraphIso}G\ne \varnothing$$
13		n0	$$⊢H\mathrm{GraphIso}G\ne \varnothing \leftrightarrow \exists ff\in \left(H\mathrm{GraphIso}G\right)$$
14	12 13	bitri	$$⊢H{\simeq }_{𝑔𝑟}G\leftrightarrow \exists ff\in \left(H\mathrm{GraphIso}G\right)$$
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 \mathrm{USGraph}$$
17		usgruhgr	$$⊢H\in \mathrm{USGraph}\to H\in \mathrm{UHGraph}$$
18	16 17	ax-mp	$$⊢H\in \mathrm{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 \mathrm{V}$$
27	26	imaex	$$⊢f\left[\left\{0,1,2\right\}\right]\in \mathrm{V}$$
28		id	$$⊢f\left[\left\{0,1,2\right\}\right]\in \mathrm{V}\to f\left[\left\{0,1,2\right\}\right]\in \mathrm{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{\simeq }_{𝑔𝑟}H\to \neg G{\simeq }_{𝑔𝑟}H$$
40	39	pm2.01i	$$⊢\neg G{\simeq }_{𝑔𝑟}H$$