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