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