This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrgrtrirex

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

Ref Expression
Hypotheses usgrgrtrirex.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgrgrtrirex.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
usgrgrtrirex.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑎 )
Assertion usgrgrtrirex ( 𝐺 ∈ USGraph → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 usgrgrtrirex.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgrgrtrirex.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 usgrgrtrirex.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑎 )
4 1 2 isgrtri ⊢ ( 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
5 4 exbii ⊢ ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑡 ∃ 𝑎 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
6 rexcom4 ⊢ ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑡 ∃ 𝑎 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
7 fveqeq2 ⊢ ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } → ( ( ♯ ‘ 𝑡 ) = 3 ↔ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ) )
8 7 adantl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ) → ( ( ♯ ‘ 𝑡 ) = 3 ↔ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ) )
9 neeq1 ⊢ ( 𝑏 = 𝑦 → ( 𝑏 ≠ 𝑐 ↔ 𝑦 ≠ 𝑐 ) )
10 preq1 ⊢ ( 𝑏 = 𝑦 → { 𝑏 , 𝑐 } = { 𝑦 , 𝑐 } )
11 10 eleq1d ⊢ ( 𝑏 = 𝑦 → ( { 𝑏 , 𝑐 } ∈ 𝐸 ↔ { 𝑦 , 𝑐 } ∈ 𝐸 ) )
12 9 11 anbi12d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ ( 𝑦 ≠ 𝑐 ∧ { 𝑦 , 𝑐 } ∈ 𝐸 ) ) )
13 neeq2 ⊢ ( 𝑐 = 𝑧 → ( 𝑦 ≠ 𝑐 ↔ 𝑦 ≠ 𝑧 ) )
14 preq2 ⊢ ( 𝑐 = 𝑧 → { 𝑦 , 𝑐 } = { 𝑦 , 𝑧 } )
15 14 eleq1d ⊢ ( 𝑐 = 𝑧 → ( { 𝑦 , 𝑐 } ∈ 𝐸 ↔ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
16 13 15 anbi12d ⊢ ( 𝑐 = 𝑧 → ( ( 𝑦 ≠ 𝑐 ∧ { 𝑦 , 𝑐 } ∈ 𝐸 ) ↔ ( 𝑦 ≠ 𝑧 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
17 prcom ⊢ { 𝑎 , 𝑦 } = { 𝑦 , 𝑎 }
18 17 eleq1i ⊢ ( { 𝑎 , 𝑦 } ∈ 𝐸 ↔ { 𝑦 , 𝑎 } ∈ 𝐸 )
19 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ { 𝑦 , 𝑎 } ∈ 𝐸 ) )
20 19 biimprcd ⊢ ( { 𝑦 , 𝑎 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
21 18 20 sylbi ⊢ ( { 𝑎 , 𝑦 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
22 21 3ad2ant1 ⊢ ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( 𝐺 ∈ USGraph → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
23 22 com12 ⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
24 23 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
25 24 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
26 25 a1d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) ) )
27 26 3imp ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑦 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
28 27 3 eleqtrrdi ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑦 ∈ 𝑁 )
29 prcom ⊢ { 𝑎 , 𝑧 } = { 𝑧 , 𝑎 }
30 29 eleq1i ⊢ ( { 𝑎 , 𝑧 } ∈ 𝐸 ↔ { 𝑧 , 𝑎 } ∈ 𝐸 )
31 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ { 𝑧 , 𝑎 } ∈ 𝐸 ) )
32 31 biimprcd ⊢ ( { 𝑧 , 𝑎 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
33 30 32 sylbi ⊢ ( { 𝑎 , 𝑧 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
34 33 3ad2ant2 ⊢ ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ( 𝐺 ∈ USGraph → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
35 34 com12 ⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
36 35 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
37 36 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
38 37 a1d ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) ) )
39 38 3imp ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑧 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
40 39 3 eleqtrrdi ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑧 ∈ 𝑁 )
41 hashtpg ⊢ ( ( 𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎 ) ↔ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ) )
42 41 bicomd ⊢ ( ( 𝑎 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ↔ ( 𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎 ) ) )
43 42 el3v ⊢ ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ↔ ( 𝑎 ≠ 𝑦 ∧ 𝑦 ≠ 𝑧 ∧ 𝑧 ≠ 𝑎 ) )
44 43 simp2bi ⊢ ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 → 𝑦 ≠ 𝑧 )
45 44 3ad2ant2 ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → 𝑦 ≠ 𝑧 )
46 simp33 ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → { 𝑦 , 𝑧 } ∈ 𝐸 )
47 45 46 jca ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ( 𝑦 ≠ 𝑧 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) )
48 12 16 28 40 47 2rspcedvdw ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
49 48 3exp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) )
50 49 adantr ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ) → ( ( ♯ ‘ { 𝑎 , 𝑦 , 𝑧 } ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) )
51 8 50 sylbid ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ∧ 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ) → ( ( ♯ ‘ 𝑡 ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) )
52 51 ex ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } → ( ( ♯ ‘ 𝑡 ) = 3 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) ) )
53 52 3impd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
54 53 rexlimdvva ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
55 54 exlimdv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) → ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
56 3 eleq2i ⊢ ( 𝑏 ∈ 𝑁 ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
57 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ { 𝑏 , 𝑎 } ∈ 𝐸 ) )
58 56 57 bitrid ⊢ ( 𝐺 ∈ USGraph → ( 𝑏 ∈ 𝑁 ↔ { 𝑏 , 𝑎 } ∈ 𝐸 ) )
59 3 eleq2i ⊢ ( 𝑐 ∈ 𝑁 ↔ 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
60 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑐 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
61 59 60 bitrid ⊢ ( 𝐺 ∈ USGraph → ( 𝑐 ∈ 𝑁 ↔ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
62 58 61 anbi12d ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) ↔ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )
63 62 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) ↔ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )
64 tpex ⊢ { 𝑎 , 𝑏 , 𝑐 } ∈ V
65 64 a1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑏 , 𝑐 } ∈ V )
66 tpeq2 ⊢ ( 𝑦 = 𝑏 → { 𝑎 , 𝑦 , 𝑧 } = { 𝑎 , 𝑏 , 𝑧 } )
67 66 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ↔ { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑧 } ) )
68 preq2 ⊢ ( 𝑦 = 𝑏 → { 𝑎 , 𝑦 } = { 𝑎 , 𝑏 } )
69 68 eleq1d ⊢ ( 𝑦 = 𝑏 → ( { 𝑎 , 𝑦 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
70 preq1 ⊢ ( 𝑦 = 𝑏 → { 𝑦 , 𝑧 } = { 𝑏 , 𝑧 } )
71 70 eleq1d ⊢ ( 𝑦 = 𝑏 → ( { 𝑦 , 𝑧 } ∈ 𝐸 ↔ { 𝑏 , 𝑧 } ∈ 𝐸 ) )
72 69 71 3anbi13d ⊢ ( 𝑦 = 𝑏 → ( ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑏 , 𝑧 } ∈ 𝐸 ) ) )
73 67 72 3anbi13d ⊢ ( 𝑦 = 𝑏 → ( ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑏 , 𝑧 } ∈ 𝐸 ) ) ) )
74 tpeq3 ⊢ ( 𝑧 = 𝑐 → { 𝑎 , 𝑏 , 𝑧 } = { 𝑎 , 𝑏 , 𝑐 } )
75 74 eqeq2d ⊢ ( 𝑧 = 𝑐 → ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑧 } ↔ { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } ) )
76 preq2 ⊢ ( 𝑧 = 𝑐 → { 𝑎 , 𝑧 } = { 𝑎 , 𝑐 } )
77 76 eleq1d ⊢ ( 𝑧 = 𝑐 → ( { 𝑎 , 𝑧 } ∈ 𝐸 ↔ { 𝑎 , 𝑐 } ∈ 𝐸 ) )
78 preq2 ⊢ ( 𝑧 = 𝑐 → { 𝑏 , 𝑧 } = { 𝑏 , 𝑐 } )
79 78 eleq1d ⊢ ( 𝑧 = 𝑐 → ( { 𝑏 , 𝑧 } ∈ 𝐸 ↔ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
80 77 79 3anbi23d ⊢ ( 𝑧 = 𝑐 → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑏 , 𝑧 } ∈ 𝐸 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
81 75 80 3anbi13d ⊢ ( 𝑧 = 𝑐 → ( ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑏 , 𝑧 } ∈ 𝐸 ) ) ↔ ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) ) )
82 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
83 82 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → 𝐺 ∈ UHGraph )
84 2 eleq2i ⊢ ( { 𝑏 , 𝑎 } ∈ 𝐸 ↔ { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
85 84 biimpi ⊢ ( { 𝑏 , 𝑎 } ∈ 𝐸 → { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
86 85 adantr ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
87 vex ⊢ 𝑏 ∈ V
88 87 prid1 ⊢ 𝑏 ∈ { 𝑏 , 𝑎 }
89 88 a1i ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ∈ { 𝑏 , 𝑎 } )
90 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑏 ∈ { 𝑏 , 𝑎 } ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
91 83 86 89 90 syl3an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
92 91 1 eleqtrrdi ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ∈ 𝑉 )
93 2 eleq2i ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 ↔ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
94 93 biimpi ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 → { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
95 94 adantl ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
96 vex ⊢ 𝑐 ∈ V
97 96 prid1 ⊢ 𝑐 ∈ { 𝑐 , 𝑎 }
98 97 a1i ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑐 ∈ { 𝑐 , 𝑎 } )
99 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑐 ∈ { 𝑐 , 𝑎 } ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
100 83 95 98 99 syl3an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
101 100 1 eleqtrrdi ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ∈ 𝑉 )
102 eqidd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } )
103 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑎 } ∈ 𝐸 ) → 𝑏 ≠ 𝑎 )
104 103 necomd ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑎 } ∈ 𝐸 ) → 𝑎 ≠ 𝑏 )
105 104 ad2ant2r ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝑎 ≠ 𝑏 )
106 105 3adant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑎 ≠ 𝑏 )
107 simpl ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 )
108 107 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ≠ 𝑐 )
109 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → 𝑐 ≠ 𝑎 )
110 109 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝑐 ≠ 𝑎 )
111 110 3adant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ≠ 𝑎 )
112 106 108 111 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) )
113 hashtpg ⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ) )
114 113 el3v ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 )
115 112 114 sylib ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 )
116 prcom ⊢ { 𝑏 , 𝑎 } = { 𝑎 , 𝑏 }
117 116 eleq1i ⊢ ( { 𝑏 , 𝑎 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 )
118 117 biimpi ⊢ ( { 𝑏 , 𝑎 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 )
119 118 adantr ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
120 119 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
121 prcom ⊢ { 𝑐 , 𝑎 } = { 𝑎 , 𝑐 }
122 121 eleq1i ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 ↔ { 𝑎 , 𝑐 } ∈ 𝐸 )
123 122 biimpi ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 → { 𝑎 , 𝑐 } ∈ 𝐸 )
124 123 adantl ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑎 , 𝑐 } ∈ 𝐸 )
125 124 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑐 } ∈ 𝐸 )
126 simpr ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → { 𝑏 , 𝑐 } ∈ 𝐸 )
127 126 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑏 , 𝑐 } ∈ 𝐸 )
128 120 125 127 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
129 102 115 128 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
130 73 81 92 101 129 2rspcedvdw ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
131 eqeq1 ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ↔ { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ) )
132 fveqeq2 ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑡 ) = 3 ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ) )
133 131 132 3anbi12d ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
134 133 2rexbidv ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
135 65 130 134 spcedv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
136 135 3exp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
137 63 136 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
138 137 rexlimdvv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
139 55 138 impbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
140 139 rexbidva ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
141 6 140 bitr3id ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑡 ∃ 𝑎 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
142 5 141 bitrid ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )