Theorem usgrgrtrirex 48570

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 48563	. . 3 ⊢ (𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
4	3	exbii 1871	. 2 ⊢ (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
5		rexcom4 3292	. . 3 ⊢ (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
6		fveqeq2 6880	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑦, 𝑧} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
7	6	adantl 486	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ 𝑡 = {𝑎, 𝑦, 𝑧}) → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
8		neeq1 3022	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → (𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐))
9		preq1 4695	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑦 → {𝑏, 𝑐} = {𝑦, 𝑐})
10	9	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑦 → ({𝑏, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑐} ∈ 𝐸))
11	8, 10	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝑦 → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸)))
12		neeq2 3023	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → (𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧))
13		preq2 4696	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑧 → {𝑦, 𝑐} = {𝑦, 𝑧})
14	13	eleq1d 2850	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑧 → ({𝑦, 𝑐} ∈ 𝐸 ↔ {𝑦, 𝑧} ∈ 𝐸))
15	12, 14	anbi12d 643	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑧 → ((𝑦 ≠ 𝑐 ∧ {𝑦, 𝑐} ∈ 𝐸) ↔ (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸)))
16		prcom 4694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑦} = {𝑦, 𝑎}
17	16	eleq1i 2856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑦, 𝑎} ∈ 𝐸)
18	2	nbusgreledg 29612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑦 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑦, 𝑎} ∈ 𝐸))
19	18	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑦, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
20	17, 19	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑦} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑦 ∈ (𝐺 NeighbVtx 𝑎)))
21	20	3ad2ant1 1149	. . . . . . . . . . . . . . . . . . 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 1126	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ (𝐺 NeighbVtx 𝑎))
27		usgrgrtrirex.n	. . . . . . . . . . . . . 14 ⊢ 𝑁 = (𝐺 NeighbVtx 𝑎)
28	26, 27	eleqtrrdi 2876	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ∈ 𝑁)
29		prcom 4694	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {𝑎, 𝑧} = {𝑧, 𝑎}
30	29	eleq1i 2856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑧, 𝑎} ∈ 𝐸)
31	2	nbusgreledg 29612	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → (𝑧 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑧, 𝑎} ∈ 𝐸))
32	31	biimprcd 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑧, 𝑎} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
33	30, 32	sylbi 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑎, 𝑧} ∈ 𝐸 → (𝐺 ∈ USGraph → 𝑧 ∈ (𝐺 NeighbVtx 𝑎)))
34	33	3ad2ant2 1150	. . . . . . . . . . . . . . . . . . 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 1126	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ (𝐺 NeighbVtx 𝑎))
40	39, 27	eleqtrrdi 2876	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑧 ∈ 𝑁)
41		hashtpg 14512	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑦, 𝑧}) = 3))
42	41	bicomd 226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎)))
43	42	el3v 3465	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 ↔ (𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎))
44	43	simp2bi 1162	. . . . . . . . . . . . . . 15 ⊢ ((♯‘{𝑎, 𝑦, 𝑧}) = 3 → 𝑦 ≠ 𝑧)
45	44	3ad2ant2 1150	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → 𝑦 ≠ 𝑧)
46		simp33 1228	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → {𝑦, 𝑧} ∈ 𝐸)
47	45, 46	jca 520	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → (𝑦 ≠ 𝑧 ∧ {𝑦, 𝑧} ∈ 𝐸))
48	11, 15, 28, 40, 47	2rspcedvdw 3598	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) ∧ (♯‘{𝑎, 𝑦, 𝑧}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸))
49	48	3exp 1135	. . . . . . . . . . 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 1365	. . . . . . 7 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
54	53	rexlimdvva 3222	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
55	54	exlimdv 1956	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) → ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
56	27	eleq2i 2857	. . . . . . . . . 10 ⊢ (𝑏 ∈ 𝑁 ↔ 𝑏 ∈ (𝐺 NeighbVtx 𝑎))
57	2	nbusgreledg 29612	. . . . . . . . . 10 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ (𝐺 NeighbVtx 𝑎) ↔ {𝑏, 𝑎} ∈ 𝐸))
58	56, 57	bitrid 286	. . . . . . . . 9 ⊢ (𝐺 ∈ USGraph → (𝑏 ∈ 𝑁 ↔ {𝑏, 𝑎} ∈ 𝐸))
59	27	eleq2i 2857	. . . . . . . . . 10 ⊢ (𝑐 ∈ 𝑁 ↔ 𝑐 ∈ (𝐺 NeighbVtx 𝑎))
60	2	nbusgreledg 29612	. . . . . . . . . 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 7733	. . . . . . . . . 10 ⊢ {𝑎, 𝑏, 𝑐} ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} ∈ V)
66		tpeq2 4705	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦, 𝑧} = {𝑎, 𝑏, 𝑧})
67	66	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧}))
68		preq2 4696	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑎, 𝑦} = {𝑎, 𝑏})
69	68	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑎, 𝑦} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸))
70		preq1 4695	. . . . . . . . . . . . 13 ⊢ (𝑦 = 𝑏 → {𝑦, 𝑧} = {𝑏, 𝑧})
71	70	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑏 → ({𝑦, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑧} ∈ 𝐸))
72	69, 71	3anbi13d 1462	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)))
73	67, 72	3anbi13d 1462	. . . . . . . . . 10 ⊢ (𝑦 = 𝑏 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸))))
74		tpeq3 4706	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑏, 𝑧} = {𝑎, 𝑏, 𝑐})
75	74	eqeq2d 2776	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐}))
76		preq2 4696	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑎, 𝑧} = {𝑎, 𝑐})
77	76	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑎, 𝑧} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸))
78		preq2 4696	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑐 → {𝑏, 𝑧} = {𝑏, 𝑐})
79	78	eleq1d 2850	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑐 → ({𝑏, 𝑧} ∈ 𝐸 ↔ {𝑏, 𝑐} ∈ 𝐸))
80	77, 79	3anbi23d 1463	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸) ↔ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
81	75, 80	3anbi13d 1462	. . . . . . . . . 10 ⊢ (𝑧 = 𝑐 → (({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑏, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))))
82		usgruhgr 29445	. . . . . . . . . . . . 13 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
83	82	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → 𝐺 ∈ UHGraph)
84	2	eleq2i 2857	. . . . . . . . . . . . 13 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑏, 𝑎} ∈ (Edg‘𝐺))
85	84	birani 508	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑏, 𝑎} ∈ (Edg‘𝐺))
86		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
87	86	prid1 4724	. . . . . . . . . . . . 13 ⊢ 𝑏 ∈ {𝑏, 𝑎}
88	87	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ∈ {𝑏, 𝑎})
89		uhgredgrnv 29389	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑏, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑏 ∈ {𝑏, 𝑎}) → 𝑏 ∈ (Vtx‘𝐺))
90	83, 85, 88, 89	syl3an 1176	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ (Vtx‘𝐺))
91	90, 1	eleqtrrdi 2876	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ∈ 𝑉)
92	2	eleq2i 2857	. . . . . . . . . . . . 13 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, 𝑎} ∈ (Edg‘𝐺))
93	92	bilani 509	. . . . . . . . . . . 12 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑐, 𝑎} ∈ (Edg‘𝐺))
94		vex 3461	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
95	94	prid1 4724	. . . . . . . . . . . . 13 ⊢ 𝑐 ∈ {𝑐, 𝑎}
96	95	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑐 ∈ {𝑐, 𝑎})
97		uhgredgrnv 29389	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ UHGraph ∧ {𝑐, 𝑎} ∈ (Edg‘𝐺) ∧ 𝑐 ∈ {𝑐, 𝑎}) → 𝑐 ∈ (Vtx‘𝐺))
98	83, 93, 96, 97	syl3an 1176	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ (Vtx‘𝐺))
99	98, 1	eleqtrrdi 2876	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ∈ 𝑉)
100		eqidd 2766	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐})
101	2	usgredgne 29465	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑏 ≠ 𝑎)
102	101	necomd 3015	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑏, 𝑎} ∈ 𝐸) → 𝑎 ≠ 𝑏)
103	102	ad2ant2r 759	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
104	103	3adant3 1148	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑎 ≠ 𝑏)
105		simpl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → 𝑏 ≠ 𝑐)
106	105	3ad2ant3 1151	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑏 ≠ 𝑐)
107	2	usgredgne 29465	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ {𝑐, 𝑎} ∈ 𝐸) → 𝑐 ≠ 𝑎)
108	107	ad2ant2rl 761	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
109	108	3adant3 1148	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → 𝑐 ≠ 𝑎)
110	104, 106, 109	3jca 1144	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))
111		hashtpg 14512	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
112	111	el3v 3465	. . . . . . . . . . . 12 ⊢ ((𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎) ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3)
113	110, 112	sylib 221	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → (♯‘{𝑎, 𝑏, 𝑐}) = 3)
114		prcom 4694	. . . . . . . . . . . . . . 15 ⊢ {𝑏, 𝑎} = {𝑎, 𝑏}
115	114	eleq1i 2856	. . . . . . . . . . . . . 14 ⊢ ({𝑏, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)
116	115	birani 508	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸)
117	116	3ad2ant2 1150	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑏} ∈ 𝐸)
118		prcom 4694	. . . . . . . . . . . . . . 15 ⊢ {𝑐, 𝑎} = {𝑎, 𝑐}
119	118	eleq1i 2856	. . . . . . . . . . . . . 14 ⊢ ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑎, 𝑐} ∈ 𝐸)
120	119	bilani 509	. . . . . . . . . . . . 13 ⊢ (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → {𝑎, 𝑐} ∈ 𝐸)
121	120	3ad2ant2 1150	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑎, 𝑐} ∈ 𝐸)
122		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → {𝑏, 𝑐} ∈ 𝐸)
123	122	3ad2ant3 1151	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → {𝑏, 𝑐} ∈ 𝐸)
124	117, 121, 123	3jca 1144	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
125	100, 113, 124	3jca 1144	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑏, 𝑐} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑎, 𝑐} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
126	73, 81, 91, 99, 125	2rspcedvdw 3598	. . . . . . . . 9 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
127		eqeq1 2769	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (𝑡 = {𝑎, 𝑦, 𝑧} ↔ {𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧}))
128		fveqeq2 6880	. . . . . . . . . . 11 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((♯‘𝑡) = 3 ↔ (♯‘{𝑎, 𝑏, 𝑐}) = 3))
129	127, 128	3anbi12d 1461	. . . . . . . . . 10 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → ((𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
130	129	2rexbidv 3230	. . . . . . . . 9 ⊢ (𝑡 = {𝑎, 𝑏, 𝑐} → (∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ({𝑎, 𝑏, 𝑐} = {𝑎, 𝑦, 𝑧} ∧ (♯‘{𝑎, 𝑏, 𝑐}) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
131	65, 126, 130	spcedv 3560	. . . . . . . 8 ⊢ (((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) ∧ ({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))
132	131	3exp 1135	. . . . . . 7 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (({𝑏, 𝑎} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
133	63, 132	sylbid 243	. . . . . 6 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → ((𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁) → ((𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)))))
134	133	rexlimdvv 3221	. . . . 5 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸) → ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸))))
135	55, 134	impbid 215	. . . 4 ⊢ ((𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉) → (∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
136	135	rexbidva 3187	. . 3 ⊢ (𝐺 ∈ USGraph → (∃𝑎 ∈ 𝑉 ∃𝑡∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
137	5, 136	bitr3id 288	. 2 ⊢ (𝐺 ∈ USGraph → (∃𝑡∃𝑎 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 (𝑡 = {𝑎, 𝑦, 𝑧} ∧ (♯‘𝑡) = 3 ∧ ({𝑎, 𝑦} ∈ 𝐸 ∧ {𝑎, 𝑧} ∈ 𝐸 ∧ {𝑦, 𝑧} ∈ 𝐸)) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))
138	4, 137	bitrid 286	1 ⊢ (𝐺 ∈ USGraph → (∃𝑡 𝑡 ∈ (GrTriangles‘𝐺) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑁 ∃𝑐 ∈ 𝑁 (𝑏 ≠ 𝑐 ∧ {𝑏, 𝑐} ∈ 𝐸)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145   ≠ wne 2960  ∃wrex 3089  Vcvv 3457  {cpr 4587  {ctp 4589  ‘cfv 6525  (class class class)co 7400  3c3 12287  ♯chash 14357  Vtxcvtx 29255  Edgcedg 29306  UHGraphcuhgr 29315  USGraphcusgr 29408   NeighbVtx cnbgr 29591  GrTrianglescgrtri 48557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pow 5327  ax-pr 5395  ax-un 7722  ax-cnex 11144  ax-resscn 11145  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-addrcl 11149  ax-mulcl 11150  ax-mulrcl 11151  ax-mulcom 11152  ax-addass 11153  ax-mulass 11154  ax-distr 11155  ax-i2m1 11156  ax-1ne0 11157  ax-1rid 11158  ax-rnegex 11159  ax-rrecex 11160  ax-cnre 11161  ax-pre-lttri 11162  ax-pre-lttrn 11163  ax-pre-ltadd 11164  ax-pre-mulgt0 11165

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4869  df-int 4909  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-lim 6355  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-riota 7357  df-ov 7403  df-oprab 7404  df-mpo 7405  df-om 7851  df-1st 7974  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346  df-rdg 8385  df-1o 8441  df-2o 8442  df-3o 8443  df-oadd 8445  df-er 8682  df-en 8932  df-dom 8933  df-sdom 8934  df-fin 8935  df-dju 9875  df-card 9913  df-pnf 11233  df-mnf 11234  df-xr 11235  df-ltxr 11236  df-le 11237  df-sub 11431  df-neg 11432  df-nn 12225  df-2 12294  df-3 12295  df-n0 12496  df-xnn0 12569  df-z 12583  df-uz 12854  df-fz 13527  df-fzo 13674  df-hash 14358  df-edg 29307  df-uhgr 29317  df-upgr 29341  df-umgr 29342  df-uspgr 29409  df-usgr 29410  df-nbgr 29592  df-grtri 48558

This theorem is referenced by:  usgrexmpl2trifr  48657  gpg3kgrtriex  48709