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 birani ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
86 vex ⊢ 𝑏 ∈ V
87 86 prid1 ⊢ 𝑏 ∈ { 𝑏 , 𝑎 }
88 87 a1i ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ∈ { 𝑏 , 𝑎 } )
89 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑏 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑏 ∈ { 𝑏 , 𝑎 } ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
90 83 85 88 89 syl3an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
91 90 1 eleqtrrdi ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ∈ 𝑉 )
92 2 eleq2i ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 ↔ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
93 92 bilani ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) )
94 vex ⊢ 𝑐 ∈ V
95 94 prid1 ⊢ 𝑐 ∈ { 𝑐 , 𝑎 }
96 95 a1i ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑐 ∈ { 𝑐 , 𝑎 } )
97 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝑐 ∈ { 𝑐 , 𝑎 } ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
98 83 93 96 97 syl3an ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
99 98 1 eleqtrrdi ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ∈ 𝑉 )
100 eqidd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } )
101 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑎 } ∈ 𝐸 ) → 𝑏 ≠ 𝑎 )
102 101 necomd ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑎 } ∈ 𝐸 ) → 𝑎 ≠ 𝑏 )
103 102 ad2ant2r ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝑎 ≠ 𝑏 )
104 103 3adant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑎 ≠ 𝑏 )
105 simpl ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 )
106 105 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑏 ≠ 𝑐 )
107 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → 𝑐 ≠ 𝑎 )
108 107 ad2ant2rl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) → 𝑐 ≠ 𝑎 )
109 108 3adant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → 𝑐 ≠ 𝑎 )
110 104 106 109 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) )
111 hashtpg ⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V ) → ( ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ) )
112 111 el3v ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎 ) ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 )
113 110 112 sylib ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 )
114 prcom ⊢ { 𝑏 , 𝑎 } = { 𝑎 , 𝑏 }
115 114 eleq1i ⊢ ( { 𝑏 , 𝑎 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 )
116 115 birani ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
117 116 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
118 prcom ⊢ { 𝑐 , 𝑎 } = { 𝑎 , 𝑐 }
119 118 eleq1i ⊢ ( { 𝑐 , 𝑎 } ∈ 𝐸 ↔ { 𝑎 , 𝑐 } ∈ 𝐸 )
120 119 bilani ⊢ ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → { 𝑎 , 𝑐 } ∈ 𝐸 )
121 120 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑎 , 𝑐 } ∈ 𝐸 )
122 simpr ⊢ ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → { 𝑏 , 𝑐 } ∈ 𝐸 )
123 122 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → { 𝑏 , 𝑐 } ∈ 𝐸 )
124 117 121 123 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
125 100 113 124 3jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑏 , 𝑐 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑎 , 𝑐 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
126 73 81 91 99 125 2rspcedvdw ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
127 eqeq1 ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ↔ { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ) )
128 fveqeq2 ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ( ♯ ‘ 𝑡 ) = 3 ↔ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ) )
129 127 128 3anbi12d ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
130 129 2rexbidv ⊢ ( 𝑡 = { 𝑎 , 𝑏 , 𝑐 } → ( ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( { 𝑎 , 𝑏 , 𝑐 } = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 𝑎 , 𝑏 , 𝑐 } ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
131 65 126 130 spcedv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) ∧ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ∧ ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) )
132 131 3exp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
133 63 132 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝑏 ∈ 𝑁 ∧ 𝑐 ∈ 𝑁 ) → ( ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) ) )
134 133 rexlimdvv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ) )
135 55 134 impbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
136 135 rexbidva ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑡 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
137 6 136 bitr3id ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑡 ∃ 𝑎 ∈ 𝑉 ∃ 𝑦 ∈ 𝑉 ∃ 𝑧 ∈ 𝑉 ( 𝑡 = { 𝑎 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ 𝑡 ) = 3 ∧ ( { 𝑎 , 𝑦 } ∈ 𝐸 ∧ { 𝑎 , 𝑧 } ∈ 𝐸 ∧ { 𝑦 , 𝑧 } ∈ 𝐸 ) ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
138 5 137 bitrid ⊢ ( 𝐺 ∈ USGraph → ( ∃ 𝑡 𝑡 ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑁 ∃ 𝑐 ∈ 𝑁 ( 𝑏 ≠ 𝑐 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )