Theorem usgrgrtrirex 48442

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 48435	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
4	3	exbii 1855	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
5		rexcom4 3267	. . 3 ⊢ (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
6		fveqeq2 6843	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
7	6	adantl 482	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
8		neeq1 2997	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → (𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐))
9		preq1 4672	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → {𝑏, 𝑐} = {𝑦, 𝑐})
10	9	eleq1d 2825	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → ({𝑏, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑐} ∈ 𝐸))
11	8, 10	anbi12d 638	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸)))
12		neeq2 2998	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → (𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧))
13		preq2 4673	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑧 → {𝑦, 𝑐} = {𝑦, 𝑧})
14	13	eleq1d 2825	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → ({𝑦, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑧} ∈ 𝐸))
15	12, 14	anbi12d 638	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑧 → ((𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸)))
16		prcom 4671	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑦} = {𝑦, 𝑎}
17	16	eleq1i 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸)
18	2	nbusgreledg 29447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑦, 𝑎} ∈ 𝐸))
19	18	biimprcd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
20	17, 19	sylbi 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
21	20	3ad2ant1 1139	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
22	21	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
23	22	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
24	23	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
25	24	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))))
26	25	3imp 1116	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))
27		usgrgrtrirex.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)
28	26, 27	eleqtrrdi 2851	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ 𝑁)
29		prcom 4671	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑧} = {𝑧, 𝑎}
30	29	eleq1i 2831	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑧, 𝑎} ∈ 𝐸)
31	2	nbusgreledg 29447	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑧 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑧, 𝑎} ∈ 𝐸))
32	31	biimprcd 251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
33	30, 32	sylbi 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑧} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
34	33	3ad2ant2 1140	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
35	34	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
36	35	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
37	36	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
38	37	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))))
39	38	3imp 1116	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))
40	39, 27	eleqtrrdi 2851	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ 𝑁)
41		hashtpg 14445	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
42	41	bicomd 224	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎)))
43	42	el3v 3440	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎))
44	43	simp2bi 1152	. . . . . . . . . . . . . . 15 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → 𝑦 ≠ 𝑧)
45	44	3ad2ant2 1140	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ≠ 𝑧)
46		simp33 1218	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → {𝑦, 𝑧} ∈ 𝐸)
47	45, 46	jca 516	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸))
48	11, 15, 28, 40, 47	2rspcedvdw 3581	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))
49	48	3exp 1125	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
50	49	adantr 481	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
51	7, 50	sylbid 241	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
52	51	ex 413	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))))
53	52	3impd 1355	. . . . . . 7 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
54	53	rexlimdvva 3197	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
55	54	exlimdv 1940	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
56	27	eleq2i 2832	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑁 ↔ 𝑏 ∈ (𝐺 NeighbVtx 𝑎))
57	2	nbusgreledg 29447	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑏, 𝑎} ∈ 𝐸))
58	56, 57	bitrid 284	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ 𝑁 ↔ {𝑏, 𝑎} ∈ 𝐸))
59	27	eleq2i 2832	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑁 ↔ 𝑐 ∈ (𝐺 NeighbVtx 𝑎))
60	2	nbusgreledg 29447	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑐, 𝑎} ∈ 𝐸))
61	59, 60	bitrid 284	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ 𝑁 ↔ {𝑐, 𝑎} ∈ 𝐸))
62	58, 61	anbi12d 638	. . . . . . . 8 ⊢ (𝐺 ∈ USGraph → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
63	62	adantr 481	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
64		tpex 7696	. . . . . . . . . 10 ⊢ {𝑎, 𝑏, 𝑐} ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} ∈ V)
66		tpeq2 4682	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦, 𝑧} = {𝑎, 𝑏, 𝑧})
67	66	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧}))
68		preq2 4673	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦} = {𝑎, 𝑏})
69	68	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸))
70		preq1 4672	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑦, 𝑧} = {𝑏, 𝑧})
71	70	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑦, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑧} ∈ 𝐸))
72	69, 71	3anbi13d 1446	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)))
73	67, 72	3anbi13d 1446	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸))))
74		tpeq3 4683	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑏, 𝑧} = {𝑎, 𝑏, 𝑐})
75	74	eqeq2d 2751	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐}))
76		preq2 4673	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑧} = {𝑎, 𝑐})
77	76	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸))
78		preq2 4673	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑏, 𝑧} = {𝑏, 𝑐})
79	78	eleq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑏, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑐} ∈ 𝐸))
80	77, 79	3anbi23d 1447	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
81	75, 80	3anbi13d 1446	. . . . . . . . . 10 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))))
82		usgruhgr 29280	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
83	82	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → 𝐺 ∈ UHGraph)
84	2	eleq2i 2832	. . . . . . . . . . . . 13 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑏, 𝑎} ∈ (Edg‘𝐺))
85	84	birani 504	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑏, 𝑎} ∈ (Edg‘𝐺))
86		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
87	86	prid1 4701	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ {𝑏, 𝑎}
88	87	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ∈ {𝑏, 𝑎})
89		uhgredgrnv 29224	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑏, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑏 ∈ {𝑏, 𝑎}) → 𝑏 ∈ (Vtx‘𝐺))
90	83, 85, 88, 89	syl3an 1166	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ (Vtx‘𝐺))
91	90, 1	eleqtrrdi 2851	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ 𝑉)
92	2	eleq2i 2832	. . . . . . . . . . . . 13 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺))
93	92	bilani 505	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑐, 𝑎} ∈ (Edg‘𝐺))
94		vex 3436	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
95	94	prid1 4701	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ {𝑐, 𝑎}
96	95	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑐 ∈ {𝑐, 𝑎})
97		uhgredgrnv 29224	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑐 ∈ {𝑐, 𝑎}) → 𝑐 ∈ (Vtx‘𝐺))
98	83, 93, 96, 97	syl3an 1166	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ (Vtx‘𝐺))
99	98, 1	eleqtrrdi 2851	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ 𝑉)
100		eqidd 2741	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐})
101	2	usgredgne 29300	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑏 ≠ 𝑎)
102	101	necomd 2990	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑎 ≠ 𝑏)
103	102	ad2ant2r 753	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
104	103	3adant3 1138	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
105		simpl 483	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ≠ 𝑐)
106	105	3ad2ant3 1141	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ≠ 𝑐)
107	2	usgredgne 29300	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑐, 𝑎} ∈ 𝐸) → 𝑐 ≠ 𝑎)
108	107	ad2ant2rl 755	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
109	108	3adant3 1138	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
110	104, 106, 109	3jca 1134	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))
111		hashtpg 14445	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
112	111	el3v 3440	. . . . . . . . . . . 12 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3)
113	110, 112	sylib 219	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (♯‘{𝑎, 𝑏, 𝑐}) = 3)
114		prcom 4671	. . . . . . . . . . . . . . 15 ⊢ {𝑏, 𝑎} = {𝑎, 𝑏}
115	114	eleq1i 2831	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)
116	115	birani 504	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸)
117	116	3ad2ant2 1140	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏} ∈ 𝐸)
118		prcom 4671	. . . . . . . . . . . . . . 15 ⊢ {𝑐, 𝑎} = {𝑎, 𝑐}
119	118	eleq1i 2831	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸)
120	119	bilani 505	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑐} ∈ 𝐸)
121	120	3ad2ant2 1140	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑐} ∈ 𝐸)
122		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → {𝑏, 𝑐} ∈ 𝐸)
123	122	3ad2ant3 1141	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑏, 𝑐} ∈ 𝐸)
124	117, 121, 123	3jca 1134	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
125	100, 113, 124	3jca 1134	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
126	73, 81, 91, 99, 125	2rspcedvdw 3581	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
127		eqeq1 2744	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (𝑡 = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧}))
128		fveqeq2 6843	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
129	127, 128	3anbi12d 1445	. . . . . . . . . 10 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
130	129	2rexbidv 3205	. . . . . . . . 9 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
131	65, 126, 130	spcedv 3543	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
132	131	3exp 1125	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
133	63, 132	sylbid 241	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
134	133	rexlimdvv 3196	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
135	55, 134	impbid 213	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
136	135	rexbidva 3162	. . 3 ⊢ (𝐺 ∈ USGraph → (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
137	5, 136	bitr3id 286	. 2 ⊢ (𝐺 ∈ USGraph → (∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
138	4, 137	bitrid 284	1 ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ∃wex 1786   ∈ wcel 2119   ≠ wne 2935  ∃wrex 3064  Vcvv 3432  {cpr 4564  {ctp 4566  ‘cfv 6492  (class class class)co 7363  3c3 12235  ♯chash 14290  Vtxcvtx 29090  Edgcedg 29141  UHGraphcuhgr 29150  USGraphcusgr 29243   NeighbVtx cnbgr 29426  GrTrianglescgrtri 48429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-rep 5206  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-cnex 11092  ax-resscn 11093  ax-1cn 11094  ax-icn 11095  ax-addcl 11096  ax-addrcl 11097  ax-mulcl 11098  ax-mulrcl 11099  ax-mulcom 11100  ax-addass 11101  ax-mulass 11102  ax-distr 11103  ax-i2m1 11104  ax-1ne0 11105  ax-1rid 11106  ax-rnegex 11107  ax-rrecex 11108  ax-cnre 11109  ax-pre-lttri 11110  ax-pre-lttrn 11111  ax-pre-ltadd 11112  ax-pre-mulgt0 11113

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-reu 3346  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-tp 4567  df-op 4569  df-uni 4846  df-int 4885  df-iun 4930  df-br 5080  df-opab 5142  df-mpt 5161  df-tr 5187  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7320  df-ov 7366  df-oprab 7367  df-mpo 7368  df-om 7814  df-1st 7938  df-2nd 7939  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-2o 8403  df-3o 8404  df-oadd 8406  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9823  df-card 9861  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183  df-sub 11377  df-neg 11378  df-nn 12173  df-2 12242  df-3 12243  df-n0 12436  df-xnn0 12509  df-z 12523  df-uz 12787  df-fz 13460  df-fzo 13607  df-hash 14291  df-edg 29142  df-uhgr 29152  df-upgr 29176  df-umgr 29177  df-uspgr 29244  df-usgr 29245  df-nbgr 29427  df-grtri 48430

This theorem is referenced by:  usgrexmpl2trifr  48529  gpg3kgrtriex  48581