Theorem usgrgrtrirex 47904

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 47897	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
4	3	exbii 1848	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
5		rexcom4 3266	. . 3 ⊢ (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
6		fveqeq2 6874	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
7	6	adantl 481	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
8		neeq1 2989	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → (𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐))
9		preq1 4705	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → {𝑏, 𝑐} = {𝑦, 𝑐})
10	9	eleq1d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → ({𝑏, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑐} ∈ 𝐸))
11	8, 10	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸)))
12		neeq2 2990	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → (𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧))
13		preq2 4706	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑧 → {𝑦, 𝑐} = {𝑦, 𝑧})
14	13	eleq1d 2814	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → ({𝑦, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑧} ∈ 𝐸))
15	12, 14	anbi12d 632	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑧 → ((𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸)))
16		prcom 4704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑦} = {𝑦, 𝑎}
17	16	eleq1i 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸)
18	2	nbusgreledg 29287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑦, 𝑎} ∈ 𝐸))
19	18	biimprcd 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
20	17, 19	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
21	20	3ad2ant1 1133	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
22	21	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
23	22	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
24	23	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
25	24	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))))
26	25	3imp 1110	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))
27		usgrgrtrirex.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)
28	26, 27	eleqtrrdi 2840	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ 𝑁)
29		prcom 4704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑧} = {𝑧, 𝑎}
30	29	eleq1i 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑧, 𝑎} ∈ 𝐸)
31	2	nbusgreledg 29287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑧 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑧, 𝑎} ∈ 𝐸))
32	31	biimprcd 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
33	30, 32	sylbi 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑧} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
34	33	3ad2ant2 1134	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
35	34	com12 32	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
36	35	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
37	36	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
38	37	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))))
39	38	3imp 1110	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))
40	39, 27	eleqtrrdi 2840	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ 𝑁)
41		hashtpg 14460	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
42	41	bicomd 223	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎)))
43	42	el3v 3463	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎))
44	43	simp2bi 1146	. . . . . . . . . . . . . . 15 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → 𝑦 ≠ 𝑧)
45	44	3ad2ant2 1134	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ≠ 𝑧)
46		simp33 1212	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → {𝑦, 𝑧} ∈ 𝐸)
47	45, 46	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸))
48	11, 15, 28, 40, 47	2rspcedvdw 3611	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))
49	48	3exp 1119	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
50	49	adantr 480	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
51	7, 50	sylbid 240	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
52	51	ex 412	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))))
53	52	3impd 1349	. . . . . . 7 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
54	53	rexlimdvva 3196	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
55	54	exlimdv 1933	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
56	27	eleq2i 2821	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑁 ↔ 𝑏 ∈ (𝐺 NeighbVtx 𝑎))
57	2	nbusgreledg 29287	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑏, 𝑎} ∈ 𝐸))
58	56, 57	bitrid 283	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ 𝑁 ↔ {𝑏, 𝑎} ∈ 𝐸))
59	27	eleq2i 2821	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑁 ↔ 𝑐 ∈ (𝐺 NeighbVtx 𝑎))
60	2	nbusgreledg 29287	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑐, 𝑎} ∈ 𝐸))
61	59, 60	bitrid 283	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ 𝑁 ↔ {𝑐, 𝑎} ∈ 𝐸))
62	58, 61	anbi12d 632	. . . . . . . 8 ⊢ (𝐺 ∈ USGraph → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
63	62	adantr 480	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
64		tpex 7729	. . . . . . . . . 10 ⊢ {𝑎, 𝑏, 𝑐} ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} ∈ V)
66		tpeq2 4715	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦, 𝑧} = {𝑎, 𝑏, 𝑧})
67	66	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧}))
68		preq2 4706	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦} = {𝑎, 𝑏})
69	68	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸))
70		preq1 4705	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑦, 𝑧} = {𝑏, 𝑧})
71	70	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑦, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑧} ∈ 𝐸))
72	69, 71	3anbi13d 1440	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)))
73	67, 72	3anbi13d 1440	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸))))
74		tpeq3 4716	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑏, 𝑧} = {𝑎, 𝑏, 𝑐})
75	74	eqeq2d 2741	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐}))
76		preq2 4706	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑧} = {𝑎, 𝑐})
77	76	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸))
78		preq2 4706	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑏, 𝑧} = {𝑏, 𝑐})
79	78	eleq1d 2814	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑏, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑐} ∈ 𝐸))
80	77, 79	3anbi23d 1441	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
81	75, 80	3anbi13d 1440	. . . . . . . . . 10 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))))
82		usgruhgr 29120	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
83	82	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → 𝐺 ∈ UHGraph)
84	2	eleq2i 2821	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑏, 𝑎} ∈ (Edg‘𝐺))
85	84	biimpi 216	. . . . . . . . . . . . 13 ⊢ ({𝑏, 𝑎} ∈ 𝐸 → {𝑏, 𝑎} ∈ (Edg‘𝐺))
86	85	adantr 480	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑏, 𝑎} ∈ (Edg‘𝐺))
87		vex 3459	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
88	87	prid1 4734	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ {𝑏, 𝑎}
89	88	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ∈ {𝑏, 𝑎})
90		uhgredgrnv 29064	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑏, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑏 ∈ {𝑏, 𝑎}) → 𝑏 ∈ (Vtx‘𝐺))
91	83, 86, 89, 90	syl3an 1160	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ (Vtx‘𝐺))
92	91, 1	eleqtrrdi 2840	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ 𝑉)
93	2	eleq2i 2821	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺))
94	93	biimpi 216	. . . . . . . . . . . . 13 ⊢ ({𝑐, 𝑎} ∈ 𝐸 → {𝑐, 𝑎} ∈ (Edg‘𝐺))
95	94	adantl 481	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑐, 𝑎} ∈ (Edg‘𝐺))
96		vex 3459	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
97	96	prid1 4734	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ {𝑐, 𝑎}
98	97	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑐 ∈ {𝑐, 𝑎})
99		uhgredgrnv 29064	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑐 ∈ {𝑐, 𝑎}) → 𝑐 ∈ (Vtx‘𝐺))
100	83, 95, 98, 99	syl3an 1160	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ (Vtx‘𝐺))
101	100, 1	eleqtrrdi 2840	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ 𝑉)
102		eqidd 2731	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐})
103	2	usgredgne 29140	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑏 ≠ 𝑎)
104	103	necomd 2982	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑎 ≠ 𝑏)
105	104	ad2ant2r 747	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
106	105	3adant3 1132	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
107		simpl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ≠ 𝑐)
108	107	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ≠ 𝑐)
109	2	usgredgne 29140	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑐, 𝑎} ∈ 𝐸) → 𝑐 ≠ 𝑎)
110	109	ad2ant2rl 749	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
111	110	3adant3 1132	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
112	106, 108, 111	3jca 1128	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))
113		hashtpg 14460	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
114	113	el3v 3463	. . . . . . . . . . . 12 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3)
115	112, 114	sylib 218	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (♯‘{𝑎, 𝑏, 𝑐}) = 3)
116		prcom 4704	. . . . . . . . . . . . . . . 16 ⊢ {𝑏, 𝑎} = {𝑎, 𝑏}
117	116	eleq1i 2820	. . . . . . . . . . . . . . 15 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)
118	117	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)
119	118	adantr 480	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸)
120	119	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏} ∈ 𝐸)
121		prcom 4704	. . . . . . . . . . . . . . . 16 ⊢ {𝑐, 𝑎} = {𝑎, 𝑐}
122	121	eleq1i 2820	. . . . . . . . . . . . . . 15 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸)
123	122	biimpi 216	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 → {𝑎, 𝑐} ∈ 𝐸)
124	123	adantl 481	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑐} ∈ 𝐸)
125	124	3ad2ant2 1134	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑐} ∈ 𝐸)
126		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → {𝑏, 𝑐} ∈ 𝐸)
127	126	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑏, 𝑐} ∈ 𝐸)
128	120, 125, 127	3jca 1128	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
129	102, 115, 128	3jca 1128	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
130	73, 81, 92, 101, 129	2rspcedvdw 3611	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
131		eqeq1 2734	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (𝑡 = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧}))
132		fveqeq2 6874	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
133	131, 132	3anbi12d 1439	. . . . . . . . . 10 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
134	133	2rexbidv 3204	. . . . . . . . 9 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
135	65, 130, 134	spcedv 3573	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
136	135	3exp 1119	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
137	63, 136	sylbid 240	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
138	137	rexlimdvv 3195	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
139	55, 138	impbid 212	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
140	139	rexbidva 3157	. . 3 ⊢ (𝐺 ∈ USGraph → (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
141	5, 140	bitr3id 285	. 2 ⊢ (𝐺 ∈ USGraph → (∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
142	4, 141	bitrid 283	1 ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2927  ∃wrex 3055  Vcvv 3455  {cpr 4599  {ctp 4601  ‘cfv 6519  (class class class)co 7394  3c3 12253  ♯chash 14305  Vtxcvtx 28930  Edgcedg 28981  UHGraphcuhgr 28990  USGraphcusgr 29083   NeighbVtx cnbgr 29266  GrTrianglescgrtri 47891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5242  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395  ax-un 7718  ax-cnex 11142  ax-resscn 11143  ax-1cn 11144  ax-icn 11145  ax-addcl 11146  ax-addrcl 11147  ax-mulcl 11148  ax-mulrcl 11149  ax-mulcom 11150  ax-addass 11151  ax-mulass 11152  ax-distr 11153  ax-i2m1 11154  ax-1ne0 11155  ax-1rid 11156  ax-rnegex 11157  ax-rrecex 11158  ax-cnre 11159  ax-pre-lttri 11160  ax-pre-lttrn 11161  ax-pre-ltadd 11162  ax-pre-mulgt0 11163

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ne 2928  df-nel 3032  df-ral 3047  df-rex 3056  df-reu 3358  df-rab 3412  df-v 3457  df-sbc 3762  df-csb 3871  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-pss 3942  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-tp 4602  df-op 4604  df-uni 4880  df-int 4919  df-iun 4965  df-br 5116  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5541  df-eprel 5546  df-po 5554  df-so 5555  df-fr 5599  df-we 5601  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-rn 5657  df-res 5658  df-ima 5659  df-pred 6282  df-ord 6343  df-on 6344  df-lim 6345  df-suc 6346  df-iota 6472  df-fun 6521  df-fn 6522  df-f 6523  df-f1 6524  df-fo 6525  df-f1o 6526  df-fv 6527  df-riota 7351  df-ov 7397  df-oprab 7398  df-mpo 7399  df-om 7851  df-1st 7977  df-2nd 7978  df-frecs 8269  df-wrecs 8300  df-recs 8349  df-rdg 8387  df-1o 8443  df-2o 8444  df-3o 8445  df-oadd 8447  df-er 8682  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-dju 9872  df-card 9910  df-pnf 11228  df-mnf 11229  df-xr 11230  df-ltxr 11231  df-le 11232  df-sub 11425  df-neg 11426  df-nn 12198  df-2 12260  df-3 12261  df-n0 12459  df-xnn0 12532  df-z 12546  df-uz 12810  df-fz 13482  df-fzo 13629  df-hash 14306  df-edg 28982  df-uhgr 28992  df-upgr 29016  df-umgr 29017  df-uspgr 29084  df-usgr 29085  df-nbgr 29267  df-grtri 47892

This theorem is referenced by:  usgrexmpl2trifr  47983  gpg3kgrtriex  48033