Metamath Proof Explorer

Theorem usgrexmpl1tri

Description: G contains a triangle 0 , 1 , 2 , with corresponding edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } . (Contributed by AV, 3-Aug-2025)

Ref Expression
Hypotheses usgrexmpl1.v 
|- V = ( 0 ... 5 )
usgrexmpl1.e 
|- E = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
usgrexmpl1.g 
|- G = <. V , E >.
Assertion usgrexmpl1tri 
|- { 0 , 1 , 2 } e. ( GrTriangles ` G )

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl1.e 
 |-  E = <" { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ">
3 usgrexmpl1.g 
 |-  G = <. V , E >.
4 c0ex 
 |-  0 e. _V
5 4 tpid1 
 |-  0 e. { 0 , 1 , 2 }
6 5 orci 
 |-  ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } )
7 elun 
 |-  ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 0 e. { 0 , 1 , 2 } \/ 0 e. { 3 , 4 , 5 } ) )
8 6 7 mpbir 
 |-  0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
9 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
10 9 orci 
 |-  ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } )
11 elun 
 |-  ( 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 1 e. { 0 , 1 , 2 } \/ 1 e. { 3 , 4 , 5 } ) )
12 10 11 mpbir 
 |-  1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
13 2ex 
 |-  2 e. _V
14 13 tpid3 
 |-  2 e. { 0 , 1 , 2 }
15 14 orci 
 |-  ( 2 e. { 0 , 1 , 2 } \/ 2 e. { 3 , 4 , 5 } )
16 elun 
 |-  ( 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) <-> ( 2 e. { 0 , 1 , 2 } \/ 2 e. { 3 , 4 , 5 } ) )
17 15 16 mpbir 
 |-  2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
18 8 12 17 3pm3.2i 
 |-  ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) )
19 eqid 
 |-  { 0 , 1 , 2 } = { 0 , 1 , 2 }
20 ex-hash 
 |-  ( # ` { 0 , 1 , 2 } ) = 3
21 prex 
 |-  { 0 , 1 } e. _V
22 21 tpid1 
 |-  { 0 , 1 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } }
23 22 orci 
 |-  ( { 0 , 1 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 0 , 1 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
24 elun 
 |-  ( { 0 , 1 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) <-> ( { 0 , 1 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 0 , 1 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
25 23 24 mpbir 
 |-  { 0 , 1 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
26 25 olci 
 |-  ( { 0 , 1 } e. { { 0 , 3 } } \/ { 0 , 1 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
27 elun 
 |-  ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> ( { 0 , 1 } e. { { 0 , 3 } } \/ { 0 , 1 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
28 26 27 mpbir 
 |-  { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
29 prex 
 |-  { 0 , 2 } e. _V
30 29 tpid2 
 |-  { 0 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } }
31 30 orci 
 |-  ( { 0 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 0 , 2 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
32 elun 
 |-  ( { 0 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) <-> ( { 0 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 0 , 2 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
33 31 32 mpbir 
 |-  { 0 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
34 33 olci 
 |-  ( { 0 , 2 } e. { { 0 , 3 } } \/ { 0 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
35 elun 
 |-  ( { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> ( { 0 , 2 } e. { { 0 , 3 } } \/ { 0 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
36 34 35 mpbir 
 |-  { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
37 prex 
 |-  { 1 , 2 } e. _V
38 37 tpid3 
 |-  { 1 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } }
39 38 orci 
 |-  ( { 1 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 1 , 2 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
40 elun 
 |-  ( { 1 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) <-> ( { 1 , 2 } e. { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } \/ { 1 , 2 } e. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
41 39 40 mpbir 
 |-  { 1 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } )
42 41 olci 
 |-  ( { 1 , 2 } e. { { 0 , 3 } } \/ { 1 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
43 elun 
 |-  ( { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> ( { 1 , 2 } e. { { 0 , 3 } } \/ { 1 , 2 } e. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
44 42 43 mpbir 
 |-  { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
45 28 36 44 3pm3.2i 
 |-  ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) )
46 19 20 45 3pm3.2i 
 |-  ( { 0 , 1 , 2 } = { 0 , 1 , 2 } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
47 tpeq1 
 |-  ( x = 0 -> { x , y , z } = { 0 , y , z } )
48 47 eqeq2d 
 |-  ( x = 0 -> ( { 0 , 1 , 2 } = { x , y , z } <-> { 0 , 1 , 2 } = { 0 , y , z } ) )
49 preq1 
 |-  ( x = 0 -> { x , y } = { 0 , y } )
50 49 eleq1d 
 |-  ( x = 0 -> ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
51 preq1 
 |-  ( x = 0 -> { x , z } = { 0 , z } )
52 51 eleq1d 
 |-  ( x = 0 -> ( { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
53 biidd 
 |-  ( x = 0 -> ( { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
54 50 52 53 3anbi123d 
 |-  ( x = 0 -> ( ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) <-> ( { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
55 48 54 3anbi13d 
 |-  ( x = 0 -> ( ( { 0 , 1 , 2 } = { x , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) <-> ( { 0 , 1 , 2 } = { 0 , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) )
56 tpeq2 
 |-  ( y = 1 -> { 0 , y , z } = { 0 , 1 , z } )
57 56 eqeq2d 
 |-  ( y = 1 -> ( { 0 , 1 , 2 } = { 0 , y , z } <-> { 0 , 1 , 2 } = { 0 , 1 , z } ) )
58 preq2 
 |-  ( y = 1 -> { 0 , y } = { 0 , 1 } )
59 58 eleq1d 
 |-  ( y = 1 -> ( { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
60 preq1 
 |-  ( y = 1 -> { y , z } = { 1 , z } )
61 60 eleq1d 
 |-  ( y = 1 -> ( { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
62 59 61 3anbi13d 
 |-  ( y = 1 -> ( ( { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) <-> ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
63 57 62 3anbi13d 
 |-  ( y = 1 -> ( ( { 0 , 1 , 2 } = { 0 , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) <-> ( { 0 , 1 , 2 } = { 0 , 1 , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) )
64 tpeq3 
 |-  ( z = 2 -> { 0 , 1 , z } = { 0 , 1 , 2 } )
65 64 eqeq2d 
 |-  ( z = 2 -> ( { 0 , 1 , 2 } = { 0 , 1 , z } <-> { 0 , 1 , 2 } = { 0 , 1 , 2 } ) )
66 biidd 
 |-  ( z = 2 -> ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
67 preq2 
 |-  ( z = 2 -> { 0 , z } = { 0 , 2 } )
68 67 eleq1d 
 |-  ( z = 2 -> ( { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
69 preq2 
 |-  ( z = 2 -> { 1 , z } = { 1 , 2 } )
70 69 eleq1d 
 |-  ( z = 2 -> ( { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) <-> { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
71 66 68 70 3anbi123d 
 |-  ( z = 2 -> ( ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) <-> ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
72 65 71 3anbi13d 
 |-  ( z = 2 -> ( ( { 0 , 1 , 2 } = { 0 , 1 , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) <-> ( { 0 , 1 , 2 } = { 0 , 1 , 2 } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) )
73 55 63 72 rspc3ev 
 |-  ( ( ( 0 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 1 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) /\ 2 e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ) /\ ( { 0 , 1 , 2 } = { 0 , 1 , 2 } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { 0 , 1 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 0 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { 1 , 2 } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) -> E. x e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. y e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. z e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { x , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
74 18 46 73 mp2an 
 |-  E. x e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. y e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. z e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { x , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
75 1 2 3 usgrexmpl1vtx 
 |-  ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } )
76 75 eqcomi 
 |-  ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) = ( Vtx ` G )
77 1 2 3 usgrexmpl1edg 
 |-  ( Edg ` G ) = ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) )
78 77 eqcomi 
 |-  ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) = ( Edg ` G )
79 76 78 isgrtri 
 |-  ( { 0 , 1 , 2 } e. ( GrTriangles ` G ) <-> E. x e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. y e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) E. z e. ( { 0 , 1 , 2 } u. { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { x , y , z } /\ ( # ` { 0 , 1 , 2 } ) = 3 /\ ( { x , y } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { x , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) /\ { y , z } e. ( { { 0 , 3 } } u. ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } u. { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
80 74 79 mpbir 
 |-  { 0 , 1 , 2 } e. ( GrTriangles ` G )