Theorem usgrgrtrirex 49124

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

Hypotheses

Ref	Expression
usgrgrtrirex.v	⊢ 𝑉 = (Vtx‘𝐺)
usgrgrtrirex.e	⊢ 𝐸 = (Edg‘𝐺)
usgrgrtrirex.n	⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)

Assertion

Ref	Expression
usgrgrtrirex	⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))

Distinct variable groups:   𝐸,𝑎,𝑏,𝑐,𝑡   𝐺,𝑎,𝑏,𝑐,𝑡   𝑁,𝑏,𝑐,𝑡   𝑉,𝑎,𝑏,𝑐,𝑡

Allowed substitution hint:   𝑁(𝑎)

Proof of Theorem usgrgrtrirex

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		usgrgrtrirex.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
2		usgrgrtrirex.e	. . . 4 ⊢ 𝐸 = (Edg‘𝐺)
3	1, 2	isgrtri 49117	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
4	3	exbii 1880	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
5		rexcom4 3289	. . 3 ⊢ (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
6		fveqeq2 6894	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
7	6	adantl 487	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
8		neeq1 3017	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → (𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐))
9		preq1 4693	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → {𝑏, 𝑐} = {𝑦, 𝑐})
10	9	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → ({𝑏, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑐} ∈ 𝐸))
11	8, 10	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸)))
12		neeq2 3018	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → (𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧))
13		preq2 4694	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑧 → {𝑦, 𝑐} = {𝑦, 𝑧})
14	13	eleq1d 2845	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → ({𝑦, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑧} ∈ 𝐸))
15	12, 14	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑧 → ((𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸)))
16		prcom 4692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑦} = {𝑦, 𝑎}
17	16	eleq1i 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸)
18	2	nbusgreledg 29935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑦, 𝑎} ∈ 𝐸))
19	18	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
20	17, 19	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
21	20	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
22	21	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
23	22	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
24	23	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
25	24	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))))
26	25	3imp 1128	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))
27		usgrgrtrirex.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)
28	26, 27	eleqtrrdi 2871	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ 𝑁)
29		prcom 4692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑧} = {𝑧, 𝑎}
30	29	eleq1i 2851	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑧, 𝑎} ∈ 𝐸)
31	2	nbusgreledg 29935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑧 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑧, 𝑎} ∈ 𝐸))
32	31	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
33	30, 32	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑧} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
34	33	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
35	34	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
36	35	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
37	36	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
38	37	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))))
39	38	3imp 1128	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))
40	39, 27	eleqtrrdi 2871	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ 𝑁)
41		hashtpg 14631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
42	41	bicomd 226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎)))
43	42	el3v 3458	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎))
44	43	simp2bi 1164	. . . . . . . . . . . . . . 15 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → 𝑦 ≠ 𝑧)
45	44	3ad2ant2 1152	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ≠ 𝑧)
46		simp33 1230	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → {𝑦, 𝑧} ∈ 𝐸)
47	45, 46	jca 521	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸))
48	11, 15, 28, 40, 47	2rspcedvdw 3589	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))
49	48	3exp 1137	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
50	49	adantr 486	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
51	7, 50	sylbid 243	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
52	51	ex 418	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))))
53	52	3impd 1367	. . . . . . 7 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
54	53	rexlimdvva 3219	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
55	54	exlimdv 1965	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
56	27	eleq2i 2852	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑁 ↔ 𝑏 ∈ (𝐺 NeighbVtx 𝑎))
57	2	nbusgreledg 29935	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑏, 𝑎} ∈ 𝐸))
58	56, 57	bitrid 286	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ 𝑁 ↔ {𝑏, 𝑎} ∈ 𝐸))
59	27	eleq2i 2852	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑁 ↔ 𝑐 ∈ (𝐺 NeighbVtx 𝑎))
60	2	nbusgreledg 29935	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑐, 𝑎} ∈ 𝐸))
61	59, 60	bitrid 286	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ 𝑁 ↔ {𝑐, 𝑎} ∈ 𝐸))
62	58, 61	anbi12d 644	. . . . . . . 8 ⊢ (𝐺 ∈ USGraph → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
63	62	adantr 486	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
64		tpex 7762	. . . . . . . . . 10 ⊢ {𝑎, 𝑏, 𝑐} ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} ∈ V)
66		tpeq2 4703	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦, 𝑧} = {𝑎, 𝑏, 𝑧})
67	66	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧}))
68		preq2 4694	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦} = {𝑎, 𝑏})
69	68	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸))
70		preq1 4693	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑦, 𝑧} = {𝑏, 𝑧})
71	70	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑦, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑧} ∈ 𝐸))
72	69, 71	3anbi13d 1466	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)))
73	67, 72	3anbi13d 1466	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸))))
74		tpeq3 4704	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑏, 𝑧} = {𝑎, 𝑏, 𝑐})
75	74	eqeq2d 2771	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐}))
76		preq2 4694	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑧} = {𝑎, 𝑐})
77	76	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸))
78		preq2 4694	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑏, 𝑧} = {𝑏, 𝑐})
79	78	eleq1d 2845	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑏, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑐} ∈ 𝐸))
80	77, 79	3anbi23d 1467	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
81	75, 80	3anbi13d 1466	. . . . . . . . . 10 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))))
82		usgruhgr 29768	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
83	82	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → 𝐺 ∈ UHGraph)
84	2	eleq2i 2852	. . . . . . . . . . . . 13 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑏, 𝑎} ∈ (Edg‘𝐺))
85	84	birani 509	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑏, 𝑎} ∈ (Edg‘𝐺))
86		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
87	86	prid1 4722	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ {𝑏, 𝑎}
88	87	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ∈ {𝑏, 𝑎})
89		uhgredgrnv 29709	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑏, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑏 ∈ {𝑏, 𝑎}) → 𝑏 ∈ (Vtx‘𝐺))
90	83, 85, 88, 89	syl3an 1178	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ (Vtx‘𝐺))
91	90, 1	eleqtrrdi 2871	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ 𝑉)
92	2	eleq2i 2852	. . . . . . . . . . . . 13 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺))
93	92	bilani 510	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑐, 𝑎} ∈ (Edg‘𝐺))
94		vex 3454	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
95	94	prid1 4722	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ {𝑐, 𝑎}
96	95	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑐 ∈ {𝑐, 𝑎})
97		uhgredgrnv 29709	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑐 ∈ {𝑐, 𝑎}) → 𝑐 ∈ (Vtx‘𝐺))
98	83, 93, 96, 97	syl3an 1178	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ (Vtx‘𝐺))
99	98, 1	eleqtrrdi 2871	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ 𝑉)
100		eqidd 2761	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐})
101	2	usgredgne 29788	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑏 ≠ 𝑎)
102	101	necomd 3010	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑎 ≠ 𝑏)
103	102	ad2ant2r 760	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
104	103	3adant3 1150	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
105		simpl 488	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ≠ 𝑐)
106	105	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ≠ 𝑐)
107	2	usgredgne 29788	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑐, 𝑎} ∈ 𝐸) → 𝑐 ≠ 𝑎)
108	107	ad2ant2rl 762	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
109	108	3adant3 1150	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
110	104, 106, 109	3jca 1146	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))
111		hashtpg 14631	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
112	111	el3v 3458	. . . . . . . . . . . 12 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3)
113	110, 112	sylib 221	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (♯‘{𝑎, 𝑏, 𝑐}) = 3)
114		prcom 4692	. . . . . . . . . . . . . . 15 ⊢ {𝑏, 𝑎} = {𝑎, 𝑏}
115	114	eleq1i 2851	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)
116	115	birani 509	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸)
117	116	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏} ∈ 𝐸)
118		prcom 4692	. . . . . . . . . . . . . . 15 ⊢ {𝑐, 𝑎} = {𝑎, 𝑐}
119	118	eleq1i 2851	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸)
120	119	bilani 510	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑐} ∈ 𝐸)
121	120	3ad2ant2 1152	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑐} ∈ 𝐸)
122		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → {𝑏, 𝑐} ∈ 𝐸)
123	122	3ad2ant3 1153	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑏, 𝑐} ∈ 𝐸)
124	117, 121, 123	3jca 1146	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
125	100, 113, 124	3jca 1146	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
126	73, 81, 91, 99, 125	2rspcedvdw 3589	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
127		eqeq1 2764	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (𝑡 = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧}))
128		fveqeq2 6894	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
129	127, 128	3anbi12d 1465	. . . . . . . . . 10 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
130	129	2rexbidv 3227	. . . . . . . . 9 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
131	65, 126, 130	spcedv 3552	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
132	131	3exp 1137	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
133	63, 132	sylbid 243	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
134	133	rexlimdvv 3218	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
135	55, 134	impbid 215	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
136	135	rexbidva 3184	. . 3 ⊢ (𝐺 ∈ USGraph → (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
137	5, 136	bitr3id 288	. 2 ⊢ (𝐺 ∈ USGraph → (∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
138	4, 137	bitrid 286	1 ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086  Vcvv 3450  {cpr 4585  {ctp 4587  ‘cfv 6538  (class class class)co 7420  3c3 12399  ♯chash 14475  Vtxcvtx 29575  Edgcedg 29626  UHGraphcuhgr 29635  USGraphcusgr 29731   NeighbVtx cnbgr 29914  GrTrianglescgrtri 49111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11257  ax-resscn 11258  ax-1cn 11259  ax-icn 11260  ax-addcl 11261  ax-addrcl 11262  ax-mulcl 11263  ax-mulrcl 11264  ax-mulcom 11265  ax-addass 11266  ax-mulass 11267  ax-distr 11268  ax-i2m1 11269  ax-1ne0 11270  ax-1rid 11271  ax-rnegex 11272  ax-rrecex 11273  ax-cnre 11274  ax-pre-lttri 11275  ax-pre-lttrn 11276  ax-pre-ltadd 11277  ax-pre-mulgt0 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-tp 4588  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8300  df-wrecs 8331  df-recs 8380  df-rdg 8419  df-1o 8477  df-2o 8478  df-3o 8479  df-oadd 8481  df-er 8718  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-dju 9983  df-card 10021  df-pnf 11346  df-mnf 11347  df-xr 11348  df-ltxr 11349  df-le 11350  df-sub 11544  df-neg 11545  df-nn 12337  df-2 12406  df-3 12407  df-n0 12608  df-xnn0 12681  df-z 12695  df-uz 12967  df-fz 13641  df-fzo 13790  df-hash 14476  df-edg 29627  df-uhgr 29637  df-upgr 29661  df-umgr 29662  df-uspgr 29732  df-usgr 29733  df-nbgr 29915  df-grtri 49112

This theorem is used by:  usgrexmpl2trifr  49211  gpg3kgrtriex  49263