Theorem usgrgrtrirex 48743

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 48736	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
4	3	exbii 1877	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
5		rexcom4 3291	. . 3 ⊢ (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
6		fveqeq2 6890	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
7	6	adantl 486	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
8		neeq1 3019	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → (𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐))
9		preq1 4698	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → {𝑏, 𝑐} = {𝑦, 𝑐})
10	9	eleq1d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → ({𝑏, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑐} ∈ 𝐸))
11	8, 10	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸)))
12		neeq2 3020	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → (𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧))
13		preq2 4699	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑧 → {𝑦, 𝑐} = {𝑦, 𝑧})
14	13	eleq1d 2847	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → ({𝑦, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑧} ∈ 𝐸))
15	12, 14	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑧 → ((𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸)))
16		prcom 4697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑦} = {𝑦, 𝑎}
17	16	eleq1i 2853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸)
18	2	nbusgreledg 29714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑦, 𝑎} ∈ 𝐸))
19	18	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
20	17, 19	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
21	20	3ad2ant1 1150	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
22	21	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
23	22	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
24	23	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
25	24	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))))
26	25	3imp 1127	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))
27		usgrgrtrirex.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)
28	26, 27	eleqtrrdi 2873	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ 𝑁)
29		prcom 4697	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑧} = {𝑧, 𝑎}
30	29	eleq1i 2853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑧, 𝑎} ∈ 𝐸)
31	2	nbusgreledg 29714	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑧 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑧, 𝑎} ∈ 𝐸))
32	31	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
33	30, 32	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑧} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
34	33	3ad2ant2 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
35	34	com12 33	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺 ∈ USGraph → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
36	35	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
37	36	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
38	37	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))))
39	38	3imp 1127	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))
40	39, 27	eleqtrrdi 2873	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ 𝑁)
41		hashtpg 14529	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
42	41	bicomd 226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎)))
43	42	el3v 3462	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎))
44	43	simp2bi 1163	. . . . . . . . . . . . . . 15 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → 𝑦 ≠ 𝑧)
45	44	3ad2ant2 1151	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ≠ 𝑧)
46		simp33 1229	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → {𝑦, 𝑧} ∈ 𝐸)
47	45, 46	jca 520	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸))
48	11, 15, 28, 40, 47	2rspcedvdw 3594	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))
49	48	3exp 1136	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
50	49	adantr 485	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
51	7, 50	sylbid 243	. . . . . . . . 9 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))))
52	51	ex 417	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))))
53	52	3impd 1366	. . . . . . 7 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
54	53	rexlimdvva 3221	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
55	54	exlimdv 1962	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
56	27	eleq2i 2854	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑁 ↔ 𝑏 ∈ (𝐺 NeighbVtx 𝑎))
57	2	nbusgreledg 29714	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑏, 𝑎} ∈ 𝐸))
58	56, 57	bitrid 286	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ 𝑁 ↔ {𝑏, 𝑎} ∈ 𝐸))
59	27	eleq2i 2854	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑁 ↔ 𝑐 ∈ (𝐺 NeighbVtx 𝑎))
60	2	nbusgreledg 29714	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑐, 𝑎} ∈ 𝐸))
61	59, 60	bitrid 286	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑐 ∈ 𝑁 ↔ {𝑐, 𝑎} ∈ 𝐸))
62	58, 61	anbi12d 643	. . . . . . . 8 ⊢ (𝐺 ∈ USGraph → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
63	62	adantr 485	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) ↔ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
64		tpex 7745	. . . . . . . . . 10 ⊢ {𝑎, 𝑏, 𝑐} ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} ∈ V)
66		tpeq2 4708	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦, 𝑧} = {𝑎, 𝑏, 𝑧})
67	66	eqeq2d 2773	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧}))
68		preq2 4699	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦} = {𝑎, 𝑏})
69	68	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸))
70		preq1 4698	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑦, 𝑧} = {𝑏, 𝑧})
71	70	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑦, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑧} ∈ 𝐸))
72	69, 71	3anbi13d 1465	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)))
73	67, 72	3anbi13d 1465	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸))))
74		tpeq3 4709	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑏, 𝑧} = {𝑎, 𝑏, 𝑐})
75	74	eqeq2d 2773	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐}))
76		preq2 4699	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑧} = {𝑎, 𝑐})
77	76	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸))
78		preq2 4699	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑏, 𝑧} = {𝑏, 𝑐})
79	78	eleq1d 2847	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑏, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑐} ∈ 𝐸))
80	77, 79	3anbi23d 1466	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
81	75, 80	3anbi13d 1465	. . . . . . . . . 10 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))))
82		usgruhgr 29547	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
83	82	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → 𝐺 ∈ UHGraph)
84	2	eleq2i 2854	. . . . . . . . . . . . 13 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑏, 𝑎} ∈ (Edg‘𝐺))
85	84	birani 508	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑏, 𝑎} ∈ (Edg‘𝐺))
86		vex 3458	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
87	86	prid1 4727	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ {𝑏, 𝑎}
88	87	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ∈ {𝑏, 𝑎})
89		uhgredgrnv 29491	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑏, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑏 ∈ {𝑏, 𝑎}) → 𝑏 ∈ (Vtx‘𝐺))
90	83, 85, 88, 89	syl3an 1177	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ (Vtx‘𝐺))
91	90, 1	eleqtrrdi 2873	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ 𝑉)
92	2	eleq2i 2854	. . . . . . . . . . . . 13 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺))
93	92	bilani 509	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑐, 𝑎} ∈ (Edg‘𝐺))
94		vex 3458	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
95	94	prid1 4727	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ {𝑐, 𝑎}
96	95	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑐 ∈ {𝑐, 𝑎})
97		uhgredgrnv 29491	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑐 ∈ {𝑐, 𝑎}) → 𝑐 ∈ (Vtx‘𝐺))
98	83, 93, 96, 97	syl3an 1177	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ (Vtx‘𝐺))
99	98, 1	eleqtrrdi 2873	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ 𝑉)
100		eqidd 2763	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐})
101	2	usgredgne 29567	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑏 ≠ 𝑎)
102	101	necomd 3012	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑎 ≠ 𝑏)
103	102	ad2ant2r 759	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
104	103	3adant3 1149	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
105		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ≠ 𝑐)
106	105	3ad2ant3 1152	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ≠ 𝑐)
107	2	usgredgne 29567	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑐, 𝑎} ∈ 𝐸) → 𝑐 ≠ 𝑎)
108	107	ad2ant2rl 761	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
109	108	3adant3 1149	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
110	104, 106, 109	3jca 1145	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))
111		hashtpg 14529	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
112	111	el3v 3462	. . . . . . . . . . . 12 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3)
113	110, 112	sylib 221	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (♯‘{𝑎, 𝑏, 𝑐}) = 3)
114		prcom 4697	. . . . . . . . . . . . . . 15 ⊢ {𝑏, 𝑎} = {𝑎, 𝑏}
115	114	eleq1i 2853	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)
116	115	birani 508	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸)
117	116	3ad2ant2 1151	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏} ∈ 𝐸)
118		prcom 4697	. . . . . . . . . . . . . . 15 ⊢ {𝑐, 𝑎} = {𝑎, 𝑐}
119	118	eleq1i 2853	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸)
120	119	bilani 509	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑐} ∈ 𝐸)
121	120	3ad2ant2 1151	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑐} ∈ 𝐸)
122		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → {𝑏, 𝑐} ∈ 𝐸)
123	122	3ad2ant3 1152	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑏, 𝑐} ∈ 𝐸)
124	117, 121, 123	3jca 1145	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
125	100, 113, 124	3jca 1145	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
126	73, 81, 91, 99, 125	2rspcedvdw 3594	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
127		eqeq1 2766	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (𝑡 = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧}))
128		fveqeq2 6890	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
129	127, 128	3anbi12d 1464	. . . . . . . . . 10 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
130	129	2rexbidv 3229	. . . . . . . . 9 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
131	65, 126, 130	spcedv 3556	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
132	131	3exp 1136	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
133	63, 132	sylbid 243	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
134	133	rexlimdvv 3220	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
135	55, 134	impbid 215	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
136	135	rexbidva 3186	. . 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 400   ∧ w3a 1102   = wceq 1569  ∃wex 1808   ∈ wcel 2142   ≠ wne 2957  ∃wrex 3088  Vcvv 3454  {cpr 4590  {ctp 4592  ‘cfv 6536  (class class class)co 7412  3c3 12302  ♯chash 14373  Vtxcvtx 29357  Edgcedg 29408  UHGraphcuhgr 29417  USGraphcusgr 29510   NeighbVtx cnbgr 29693  GrTrianglescgrtri 48730

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-reu 3369  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5555  df-eprel 5560  df-po 5568  df-so 5569  df-fr 5613  df-we 5615  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8276  df-wrecs 8307  df-recs 8356  df-rdg 8395  df-1o 8451  df-2o 8452  df-3o 8453  df-oadd 8455  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9894  df-card 9932  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11449  df-neg 11450  df-nn 12240  df-2 12309  df-3 12310  df-n0 12511  df-xnn0 12584  df-z 12598  df-uz 12869  df-fz 13542  df-fzo 13690  df-hash 14374  df-edg 29409  df-uhgr 29419  df-upgr 29443  df-umgr 29444  df-uspgr 29511  df-usgr 29512  df-nbgr 29694  df-grtri 48731

This theorem is used by:  usgrexmpl2trifr  48830  gpg3kgrtriex  48882