usgrgrtrirex

Description: Conditions for a simple graph to contain a triangle. (Contributed by AV, 7-Aug-2025)

	Ref	Expression
Hypotheses	usgrgrtrirex.v	$⊢ V = Vtx (G)$
	usgrgrtrirex.e	$⊢ E = Edg (G)$
	usgrgrtrirex.n	$⊢ N = G NeighbVtx a$
Assertion	usgrgrtrirex	Could not format assertion : No typesetting found for \|- ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. V E. b e. N E. c e. N ( b =/= c /\ { b , c } e. E ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		usgrgrtrirex.v	$⊢ V = Vtx (G)$
2		usgrgrtrirex.e	$⊢ E = Edg (G)$
3		usgrgrtrirex.n	$⊢ N = G NeighbVtx a$
4	1 2	isgrtri	Could not format ( t e. ( GrTriangles ` G ) <-> E. a e. V E. y e. V E. z e. V ( t = { a , y , z } /\ ( # ` t ) = 3 /\ ( { a , y } e. E /\ { a , z } e. E /\ { y , z } e. E ) ) ) : No typesetting found for \|- ( t e. ( GrTriangles ` G ) <-> E. a e. V E. y e. V E. z e. V ( t = { a , y , z } /\ ( # ` t ) = 3 /\ ( { a , y } e. E /\ { a , z } e. E /\ { y , z } e. E ) ) ) with typecode \|-
5	4	exbii	Could not format ( E. t t e. ( GrTriangles ` G ) <-> E. t E. a e. V E. y e. V E. z e. V ( t = { a , y , z } /\ ( # ` t ) = 3 /\ ( { a , y } e. E /\ { a , z } e. E /\ { y , z } e. E ) ) ) : No typesetting found for \|- ( E. t t e. ( GrTriangles ` G ) <-> E. t E. a e. V E. y e. V E. z e. V ( t = { a , y , z } /\ ( # ` t ) = 3 /\ ( { a , y } e. E /\ { a , z } e. E /\ { y , z } e. E ) ) ) with typecode \|-
6		rexcom4	$⊢ \exists a \in V \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow \exists t \exists a \in V \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E))$
7		fveqeq2	$⊢ t = \{a, y, z\} \to (\|t\| = 3 \leftrightarrow \|\{a, y, z\}\| = 3)$
8	7	adantl	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land t = \{a, y, z\}) \to (\|t\| = 3 \leftrightarrow \|\{a, y, z\}\| = 3)$
9		neeq1	$⊢ b = y \to (b \neq c \leftrightarrow y \neq c)$
10		preq1	$⊢ b = y \to \{b, c\} = \{y, c\}$
11	10	eleq1d	$⊢ b = y \to (\{b, c\} \in E \leftrightarrow \{y, c\} \in E)$
12	9 11	anbi12d	$⊢ b = y \to ((b \neq c \land \{b, c\} \in E) \leftrightarrow (y \neq c \land \{y, c\} \in E))$
13		neeq2	$⊢ c = z \to (y \neq c \leftrightarrow y \neq z)$
14		preq2	$⊢ c = z \to \{y, c\} = \{y, z\}$
15	14	eleq1d	$⊢ c = z \to (\{y, c\} \in E \leftrightarrow \{y, z\} \in E)$
16	13 15	anbi12d	$⊢ c = z \to ((y \neq c \land \{y, c\} \in E) \leftrightarrow (y \neq z \land \{y, z\} \in E))$
17		prcom	$⊢ \{a, y\} = \{y, a\}$
18	17	eleq1i	$⊢ \{a, y\} \in E \leftrightarrow \{y, a\} \in E$
19	2	nbusgreledg	$⊢ G \in USGraph \to (y \in (G NeighbVtx a) \leftrightarrow \{y, a\} \in E)$
20	19	biimprcd	$⊢ \{y, a\} \in E \to (G \in USGraph \to y \in (G NeighbVtx a))$
21	18 20	sylbi	$⊢ \{a, y\} \in E \to (G \in USGraph \to y \in (G NeighbVtx a))$
22	21	3ad2ant1	$⊢ (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to (G \in USGraph \to y \in (G NeighbVtx a))$
23	22	com12	$⊢ G \in USGraph \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to y \in (G NeighbVtx a))$
24	23	adantr	$⊢ (G \in USGraph \land a \in V) \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to y \in (G NeighbVtx a))$
25	24	adantr	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to y \in (G NeighbVtx a))$
26	25	a1d	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to (\|\{a, y, z\}\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to y \in (G NeighbVtx a)))$
27	26	3imp	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to y \in (G NeighbVtx a)$
28	27 3	eleqtrrdi	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to y \in N$
29		prcom	$⊢ \{a, z\} = \{z, a\}$
30	29	eleq1i	$⊢ \{a, z\} \in E \leftrightarrow \{z, a\} \in E$
31	2	nbusgreledg	$⊢ G \in USGraph \to (z \in (G NeighbVtx a) \leftrightarrow \{z, a\} \in E)$
32	31	biimprcd	$⊢ \{z, a\} \in E \to (G \in USGraph \to z \in (G NeighbVtx a))$
33	30 32	sylbi	$⊢ \{a, z\} \in E \to (G \in USGraph \to z \in (G NeighbVtx a))$
34	33	3ad2ant2	$⊢ (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to (G \in USGraph \to z \in (G NeighbVtx a))$
35	34	com12	$⊢ G \in USGraph \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to z \in (G NeighbVtx a))$
36	35	adantr	$⊢ (G \in USGraph \land a \in V) \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to z \in (G NeighbVtx a))$
37	36	adantr	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to z \in (G NeighbVtx a))$
38	37	a1d	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to (\|\{a, y, z\}\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to z \in (G NeighbVtx a)))$
39	38	3imp	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to z \in (G NeighbVtx a)$
40	39 3	eleqtrrdi	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to z \in N$
41		hashtpg	$⊢ (a \in V \land y \in V \land z \in V) \to ((a \neq y \land y \neq z \land z \neq a) \leftrightarrow \|\{a, y, z\}\| = 3)$
42	41	bicomd	$⊢ (a \in V \land y \in V \land z \in V) \to (\|\{a, y, z\}\| = 3 \leftrightarrow (a \neq y \land y \neq z \land z \neq a))$
43	42	el3v	$⊢ \|\{a, y, z\}\| = 3 \leftrightarrow (a \neq y \land y \neq z \land z \neq a)$
44	43	simp2bi	$⊢ \|\{a, y, z\}\| = 3 \to y \neq z$
45	44	3ad2ant2	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to y \neq z$
46		simp33	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to \{y, z\} \in E$
47	45 46	jca	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to (y \neq z \land \{y, z\} \in E)$
48	12 16 28 40 47	2rspcedvdw	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land \|\{a, y, z\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E)$
49	48	3exp	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to (\|\{a, y, z\}\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E)))$
50	49	adantr	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land t = \{a, y, z\}) \to (\|\{a, y, z\}\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E)))$
51	8 50	sylbid	$⊢ (((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \land t = \{a, y, z\}) \to (\|t\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E)))$
52	51	ex	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to (t = \{a, y, z\} \to (\|t\| = 3 \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))))$
53	52	3impd	$⊢ ((G \in USGraph \land a \in V) \land (y \in V \land z \in V)) \to ((t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
54	53	rexlimdvva	$⊢ (G \in USGraph \land a \in V) \to (\exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
55	54	exlimdv	$⊢ (G \in USGraph \land a \in V) \to (\exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \to \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
56	3	eleq2i	$⊢ b \in N \leftrightarrow b \in (G NeighbVtx a)$
57	2	nbusgreledg	$⊢ G \in USGraph \to (b \in (G NeighbVtx a) \leftrightarrow \{b, a\} \in E)$
58	56 57	bitrid	$⊢ G \in USGraph \to (b \in N \leftrightarrow \{b, a\} \in E)$
59	3	eleq2i	$⊢ c \in N \leftrightarrow c \in (G NeighbVtx a)$
60	2	nbusgreledg	$⊢ G \in USGraph \to (c \in (G NeighbVtx a) \leftrightarrow \{c, a\} \in E)$
61	59 60	bitrid	$⊢ G \in USGraph \to (c \in N \leftrightarrow \{c, a\} \in E)$
62	58 61	anbi12d	$⊢ G \in USGraph \to ((b \in N \land c \in N) \leftrightarrow (\{b, a\} \in E \land \{c, a\} \in E))$
63	62	adantr	$⊢ (G \in USGraph \land a \in V) \to ((b \in N \land c \in N) \leftrightarrow (\{b, a\} \in E \land \{c, a\} \in E))$
64		tpex	$⊢ \{a, b, c\} \in V$
65	64	a1i	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \{a, b, c\} \in V$
66		tpeq2	$⊢ y = b \to \{a, y, z\} = \{a, b, z\}$
67	66	eqeq2d	$⊢ y = b \to (\{a, b, c\} = \{a, y, z\} \leftrightarrow \{a, b, c\} = \{a, b, z\})$
68		preq2	$⊢ y = b \to \{a, y\} = \{a, b\}$
69	68	eleq1d	$⊢ y = b \to (\{a, y\} \in E \leftrightarrow \{a, b\} \in E)$
70		preq1	$⊢ y = b \to \{y, z\} = \{b, z\}$
71	70	eleq1d	$⊢ y = b \to (\{y, z\} \in E \leftrightarrow \{b, z\} \in E)$
72	69 71	3anbi13d	$⊢ y = b \to ((\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E) \leftrightarrow (\{a, b\} \in E \land \{a, z\} \in E \land \{b, z\} \in E))$
73	67 72	3anbi13d	$⊢ y = b \to ((\{a, b, c\} = \{a, y, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow (\{a, b, c\} = \{a, b, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, b\} \in E \land \{a, z\} \in E \land \{b, z\} \in E)))$
74		tpeq3	$⊢ z = c \to \{a, b, z\} = \{a, b, c\}$
75	74	eqeq2d	$⊢ z = c \to (\{a, b, c\} = \{a, b, z\} \leftrightarrow \{a, b, c\} = \{a, b, c\})$
76		preq2	$⊢ z = c \to \{a, z\} = \{a, c\}$
77	76	eleq1d	$⊢ z = c \to (\{a, z\} \in E \leftrightarrow \{a, c\} \in E)$
78		preq2	$⊢ z = c \to \{b, z\} = \{b, c\}$
79	78	eleq1d	$⊢ z = c \to (\{b, z\} \in E \leftrightarrow \{b, c\} \in E)$
80	77 79	3anbi23d	$⊢ z = c \to ((\{a, b\} \in E \land \{a, z\} \in E \land \{b, z\} \in E) \leftrightarrow (\{a, b\} \in E \land \{a, c\} \in E \land \{b, c\} \in E))$
81	75 80	3anbi13d	$⊢ z = c \to ((\{a, b, c\} = \{a, b, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, b\} \in E \land \{a, z\} \in E \land \{b, z\} \in E)) \leftrightarrow (\{a, b, c\} = \{a, b, c\} \land \|\{a, b, c\}\| = 3 \land (\{a, b\} \in E \land \{a, c\} \in E \land \{b, c\} \in E)))$
82		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
83	82	adantr	$⊢ (G \in USGraph \land a \in V) \to G \in UHGraph$
84	2	eleq2i	$⊢ \{b, a\} \in E \leftrightarrow \{b, a\} \in Edg (G)$
85	84	biimpi	$⊢ \{b, a\} \in E \to \{b, a\} \in Edg (G)$
86	85	adantr	$⊢ (\{b, a\} \in E \land \{c, a\} \in E) \to \{b, a\} \in Edg (G)$
87		vex	$⊢ b \in V$
88	87	prid1	$⊢ b \in \{b, a\}$
89	88	a1i	$⊢ (b \neq c \land \{b, c\} \in E) \to b \in \{b, a\}$
90		uhgredgrnv	$⊢ (G \in UHGraph \land \{b, a\} \in Edg (G) \land b \in \{b, a\}) \to b \in Vtx (G)$
91	83 86 89 90	syl3an	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to b \in Vtx (G)$
92	91 1	eleqtrrdi	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to b \in V$
93	2	eleq2i	$⊢ \{c, a\} \in E \leftrightarrow \{c, a\} \in Edg (G)$
94	93	biimpi	$⊢ \{c, a\} \in E \to \{c, a\} \in Edg (G)$
95	94	adantl	$⊢ (\{b, a\} \in E \land \{c, a\} \in E) \to \{c, a\} \in Edg (G)$
96		vex	$⊢ c \in V$
97	96	prid1	$⊢ c \in \{c, a\}$
98	97	a1i	$⊢ (b \neq c \land \{b, c\} \in E) \to c \in \{c, a\}$
99		uhgredgrnv	$⊢ (G \in UHGraph \land \{c, a\} \in Edg (G) \land c \in \{c, a\}) \to c \in Vtx (G)$
100	83 95 98 99	syl3an	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to c \in Vtx (G)$
101	100 1	eleqtrrdi	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to c \in V$
102		eqidd	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \{a, b, c\} = \{a, b, c\}$
103	2	usgredgne	$⊢ (G \in USGraph \land \{b, a\} \in E) \to b \neq a$
104	103	necomd	$⊢ (G \in USGraph \land \{b, a\} \in E) \to a \neq b$
105	104	ad2ant2r	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E)) \to a \neq b$
106	105	3adant3	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to a \neq b$
107		simpl	$⊢ (b \neq c \land \{b, c\} \in E) \to b \neq c$
108	107	3ad2ant3	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to b \neq c$
109	2	usgredgne	$⊢ (G \in USGraph \land \{c, a\} \in E) \to c \neq a$
110	109	ad2ant2rl	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E)) \to c \neq a$
111	110	3adant3	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to c \neq a$
112	106 108 111	3jca	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to (a \neq b \land b \neq c \land c \neq a)$
113		hashtpg	$⊢ (a \in V \land b \in V \land c \in V) \to ((a \neq b \land b \neq c \land c \neq a) \leftrightarrow \|\{a, b, c\}\| = 3)$
114	113	el3v	$⊢ (a \neq b \land b \neq c \land c \neq a) \leftrightarrow \|\{a, b, c\}\| = 3$
115	112 114	sylib	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \|\{a, b, c\}\| = 3$
116		prcom	$⊢ \{b, a\} = \{a, b\}$
117	116	eleq1i	$⊢ \{b, a\} \in E \leftrightarrow \{a, b\} \in E$
118	117	biimpi	$⊢ \{b, a\} \in E \to \{a, b\} \in E$
119	118	adantr	$⊢ (\{b, a\} \in E \land \{c, a\} \in E) \to \{a, b\} \in E$
120	119	3ad2ant2	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \{a, b\} \in E$
121		prcom	$⊢ \{c, a\} = \{a, c\}$
122	121	eleq1i	$⊢ \{c, a\} \in E \leftrightarrow \{a, c\} \in E$
123	122	biimpi	$⊢ \{c, a\} \in E \to \{a, c\} \in E$
124	123	adantl	$⊢ (\{b, a\} \in E \land \{c, a\} \in E) \to \{a, c\} \in E$
125	124	3ad2ant2	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \{a, c\} \in E$
126		simpr	$⊢ (b \neq c \land \{b, c\} \in E) \to \{b, c\} \in E$
127	126	3ad2ant3	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \{b, c\} \in E$
128	120 125 127	3jca	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to (\{a, b\} \in E \land \{a, c\} \in E \land \{b, c\} \in E)$
129	102 115 128	3jca	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to (\{a, b, c\} = \{a, b, c\} \land \|\{a, b, c\}\| = 3 \land (\{a, b\} \in E \land \{a, c\} \in E \land \{b, c\} \in E))$
130	73 81 92 101 129	2rspcedvdw	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \exists y \in V \exists z \in V (\{a, b, c\} = \{a, y, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E))$
131		eqeq1	$⊢ t = \{a, b, c\} \to (t = \{a, y, z\} \leftrightarrow \{a, b, c\} = \{a, y, z\})$
132		fveqeq2	$⊢ t = \{a, b, c\} \to (\|t\| = 3 \leftrightarrow \|\{a, b, c\}\| = 3)$
133	131 132	3anbi12d	$⊢ t = \{a, b, c\} \to ((t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow (\{a, b, c\} = \{a, y, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)))$
134	133	2rexbidv	$⊢ t = \{a, b, c\} \to (\exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow \exists y \in V \exists z \in V (\{a, b, c\} = \{a, y, z\} \land \|\{a, b, c\}\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)))$
135	65 130 134	spcedv	$⊢ ((G \in USGraph \land a \in V) \land (\{b, a\} \in E \land \{c, a\} \in E) \land (b \neq c \land \{b, c\} \in E)) \to \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E))$
136	135	3exp	$⊢ (G \in USGraph \land a \in V) \to ((\{b, a\} \in E \land \{c, a\} \in E) \to ((b \neq c \land \{b, c\} \in E) \to \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E))))$
137	63 136	sylbid	$⊢ (G \in USGraph \land a \in V) \to ((b \in N \land c \in N) \to ((b \neq c \land \{b, c\} \in E) \to \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E))))$
138	137	rexlimdvv	$⊢ (G \in USGraph \land a \in V) \to (\exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E) \to \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)))$
139	55 138	impbid	$⊢ (G \in USGraph \land a \in V) \to (\exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
140	139	rexbidva	$⊢ G \in USGraph \to (\exists a \in V \exists t \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow \exists a \in V \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
141	6 140	bitr3id	$⊢ G \in USGraph \to (\exists t \exists a \in V \exists y \in V \exists z \in V (t = \{a, y, z\} \land \|t\| = 3 \land (\{a, y\} \in E \land \{a, z\} \in E \land \{y, z\} \in E)) \leftrightarrow \exists a \in V \exists b \in N \exists c \in N (b \neq c \land \{b, c\} \in E))$
142	5 141	bitrid	Could not format ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. V E. b e. N E. c e. N ( b =/= c /\ { b , c } e. E ) ) ) : No typesetting found for \|- ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. V E. b e. N E. c e. N ( b =/= c /\ { b , c } e. E ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem usgrgrtrirex

Proof