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 
|- V = ( Vtx ` G )
usgrgrtrirex.e 
|- E = ( Edg ` G )
usgrgrtrirex.n 
|- N = ( G NeighbVtx a )
Assertion usgrgrtrirex 
|- ( G e. USGraph -> ( E. t t e. ( GrTriangles ` G ) <-> E. a e. V E. b e. N E. c e. N ( b =/= c /\ { b , c } e. E ) ) )

Proof

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