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 Could not format assertion : No typesetting found for |- { 0 , 1 , 2 } e. ( GrTriangles ` G ) with typecode |-

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 ∈ V
5 4 tpid1 ⊢ 0 ∈ 0 1 2
6 5 orci ⊢ 0 ∈ 0 1 2 ∨ 0 ∈ 3 4 5
7 elun ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ↔ 0 ∈ 0 1 2 ∨ 0 ∈ 3 4 5
8 6 7 mpbir ⊢ 0 ∈ 0 1 2 ∪ 3 4 5
9 1eltp012 ⊢ 1 ∈ 0 1 2
10 9 orci ⊢ 1 ∈ 0 1 2 ∨ 1 ∈ 3 4 5
11 elun ⊢ 1 ∈ 0 1 2 ∪ 3 4 5 ↔ 1 ∈ 0 1 2 ∨ 1 ∈ 3 4 5
12 10 11 mpbir ⊢ 1 ∈ 0 1 2 ∪ 3 4 5
13 2ex ⊢ 2 ∈ V
14 13 tpid3 ⊢ 2 ∈ 0 1 2
15 14 orci ⊢ 2 ∈ 0 1 2 ∨ 2 ∈ 3 4 5
16 elun ⊢ 2 ∈ 0 1 2 ∪ 3 4 5 ↔ 2 ∈ 0 1 2 ∨ 2 ∈ 3 4 5
17 15 16 mpbir ⊢ 2 ∈ 0 1 2 ∪ 3 4 5
18 8 12 17 3pm3.2i ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 2 ∈ 0 1 2 ∪ 3 4 5
19 eqid ⊢ 0 1 2 = 0 1 2
20 ex-hash ⊢ 0 1 2 = 3
21 prex ⊢ 0 1 ∈ V
22 21 tpid1 ⊢ 0 1 ∈ 0 1 0 2 1 2
23 22 orci ⊢ 0 1 ∈ 0 1 0 2 1 2 ∨ 0 1 ∈ 3 4 3 5 4 5
24 elun ⊢ 0 1 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 1 0 2 1 2 ∨ 0 1 ∈ 3 4 3 5 4 5
25 23 24 mpbir ⊢ 0 1 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
26 25 olci ⊢ 0 1 ∈ 0 3 ∨ 0 1 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
27 elun ⊢ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 3 ∨ 0 1 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
28 26 27 mpbir ⊢ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
29 prex ⊢ 0 2 ∈ V
30 29 tpid2 ⊢ 0 2 ∈ 0 1 0 2 1 2
31 30 orci ⊢ 0 2 ∈ 0 1 0 2 1 2 ∨ 0 2 ∈ 3 4 3 5 4 5
32 elun ⊢ 0 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 2 ∈ 0 1 0 2 1 2 ∨ 0 2 ∈ 3 4 3 5 4 5
33 31 32 mpbir ⊢ 0 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
34 33 olci ⊢ 0 2 ∈ 0 3 ∨ 0 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
35 elun ⊢ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 2 ∈ 0 3 ∨ 0 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
36 34 35 mpbir ⊢ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
37 prex ⊢ 1 2 ∈ V
38 37 tpid3 ⊢ 1 2 ∈ 0 1 0 2 1 2
39 38 orci ⊢ 1 2 ∈ 0 1 0 2 1 2 ∨ 1 2 ∈ 3 4 3 5 4 5
40 elun ⊢ 1 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 1 2 ∈ 0 1 0 2 1 2 ∨ 1 2 ∈ 3 4 3 5 4 5
41 39 40 mpbir ⊢ 1 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
42 41 olci ⊢ 1 2 ∈ 0 3 ∨ 1 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
43 elun ⊢ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 1 2 ∈ 0 3 ∨ 1 2 ∈ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
44 42 43 mpbir ⊢ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
45 28 36 44 3pm3.2i ⊢ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
46 19 20 45 3pm3.2i ⊢ 0 1 2 = 0 1 2 ∧ 0 1 2 = 3 ∧ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 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 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
51 preq1 ⊢ x = 0 → x z = 0 z
52 51 eleq1d ⊢ x = 0 → x z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
53 biidd ⊢ x = 0 → y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
54 50 52 53 3anbi123d ⊢ x = 0 → x y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ x z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
55 48 54 3anbi13d ⊢ x = 0 → 0 1 2 = x y z ∧ 0 1 2 = 3 ∧ x y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ x z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 2 = 0 y z ∧ 0 1 2 = 3 ∧ 0 y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 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 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
60 preq1 ⊢ y = 1 → y z = 1 z
61 60 eleq1d ⊢ y = 1 → y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
62 59 61 3anbi13d ⊢ y = 1 → 0 y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
63 57 62 3anbi13d ⊢ y = 1 → 0 1 2 = 0 y z ∧ 0 1 2 = 3 ∧ 0 y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 2 = 0 1 z ∧ 0 1 2 = 3 ∧ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 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 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
67 preq2 ⊢ z = 2 → 0 z = 0 2
68 67 eleq1d ⊢ z = 2 → 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
69 preq2 ⊢ z = 2 → 1 z = 1 2
70 69 eleq1d ⊢ z = 2 → 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
71 66 68 70 3anbi123d ⊢ z = 2 → 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
72 65 71 3anbi13d ⊢ z = 2 → 0 1 2 = 0 1 z ∧ 0 1 2 = 3 ∧ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ↔ 0 1 2 = 0 1 2 ∧ 0 1 2 = 3 ∧ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
73 55 63 72 rspc3ev ⊢ 0 ∈ 0 1 2 ∪ 3 4 5 ∧ 1 ∈ 0 1 2 ∪ 3 4 5 ∧ 2 ∈ 0 1 2 ∪ 3 4 5 ∧ 0 1 2 = 0 1 2 ∧ 0 1 2 = 3 ∧ 0 1 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 0 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ 1 2 ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 → ∃ x ∈ 0 1 2 ∪ 3 4 5 ∃ y ∈ 0 1 2 ∪ 3 4 5 ∃ z ∈ 0 1 2 ∪ 3 4 5 0 1 2 = x y z ∧ 0 1 2 = 3 ∧ x y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ x z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
74 18 46 73 mp2an ⊢ ∃ x ∈ 0 1 2 ∪ 3 4 5 ∃ y ∈ 0 1 2 ∪ 3 4 5 ∃ z ∈ 0 1 2 ∪ 3 4 5 0 1 2 = x y z ∧ 0 1 2 = 3 ∧ x y ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ x z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 ∧ y z ∈ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
75 1 2 3 usgrexmpl1vtx ⊢ Vtx ⁡ G = 0 1 2 ∪ 3 4 5
76 75 eqcomi ⊢ 0 1 2 ∪ 3 4 5 = Vtx ⁡ G
77 1 2 3 usgrexmpl1edg ⊢ Edg ⁡ G = 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5
78 77 eqcomi ⊢ 0 3 ∪ 0 1 0 2 1 2 ∪ 3 4 3 5 4 5 = Edg ⁡ G
79 76 78 isgrtri Could not format ( { 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 } } ) ) ) ) ) : No typesetting found for |- ( { 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 } } ) ) ) ) ) with typecode |-
80 74 79 mpbir Could not format { 0 , 1 , 2 } e. ( GrTriangles ` G ) : No typesetting found for |- { 0 , 1 , 2 } e. ( GrTriangles ` G ) with typecode |-