This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
usgrexmpl1.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpl1tri { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐺 )

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
3 usgrexmpl1.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
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 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑦 , 𝑧 } = { 0 , 𝑦 , 𝑧 } )
49 48 eqeq2d ⊢ ( 𝑥 = 0 → ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ) )
50 preq1 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑦 } = { 0 , 𝑦 } )
51 50 eleq1d ⊢ ( 𝑥 = 0 → ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ↔ { 0 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
52 preq1 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑧 } = { 0 , 𝑧 } )
53 52 eleq1d ⊢ ( 𝑥 = 0 → ( { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ↔ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
54 biidd ⊢ ( 𝑥 = 0 → ( { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ↔ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
55 51 53 54 3anbi123d ⊢ ( 𝑥 = 0 → ( ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ↔ ( { 0 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
56 49 55 3anbi13d ⊢ ( 𝑥 = 0 → ( ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ↔ ( { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 0 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) )
57 tpeq2 ⊢ ( 𝑦 = 1 → { 0 , 𝑦 , 𝑧 } = { 0 , 1 , 𝑧 } )
58 57 eqeq2d ⊢ ( 𝑦 = 1 → ( { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ) )
59 preq2 ⊢ ( 𝑦 = 1 → { 0 , 𝑦 } = { 0 , 1 } )
60 59 eleq1d ⊢ ( 𝑦 = 1 → ( { 0 , 𝑦 } ∈ ( { { 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 ⊢ ( 𝑦 = 1 → { 𝑦 , 𝑧 } = { 1 , 𝑧 } )
62 61 eleq1d ⊢ ( 𝑦 = 1 → ( { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ↔ { 1 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
63 60 62 3anbi13d ⊢ ( 𝑦 = 1 → ( ( { 0 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 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 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 1 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
64 58 63 3anbi13d ⊢ ( 𝑦 = 1 → ( ( { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 0 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ↔ ( { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 0 , 1 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 1 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) ) )
65 tpeq3 ⊢ ( 𝑧 = 2 → { 0 , 1 , 𝑧 } = { 0 , 1 , 2 } )
66 65 eqeq2d ⊢ ( 𝑧 = 2 → ( { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 1 , 2 } ) )
67 biidd ⊢ ( 𝑧 = 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 ⊢ ( 𝑧 = 2 → { 0 , 𝑧 } = { 0 , 2 } )
69 68 eleq1d ⊢ ( 𝑧 = 2 → ( { 0 , 𝑧 } ∈ ( { { 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 ⊢ ( 𝑧 = 2 → { 1 , 𝑧 } = { 1 , 2 } )
71 70 eleq1d ⊢ ( 𝑧 = 2 → ( { 1 , 𝑧 } ∈ ( { { 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 ⊢ ( 𝑧 = 2 → ( ( { 0 , 1 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 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 } } ) ) ∧ { 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 ⊢ ( 𝑧 = 2 → ( ( { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 0 , 1 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 0 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 1 , 𝑧 } ∈ ( { { 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 } } ) ) ) ) ) → ∃ 𝑥 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑦 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑧 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
75 19 47 74 mp2an ⊢ ∃ 𝑥 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑦 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑧 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) )
76 1 2 3 usgrexmpl1vtx ⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
77 76 eqcomi ⊢ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) = ( Vtx ‘ 𝐺 )
78 1 2 3 usgrexmpl1edg ⊢ ( Edg ‘ 𝐺 ) = ( { { 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 ‘ 𝐺 )
80 77 79 isgrtri ⊢ ( { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑦 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∃ 𝑧 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ∧ ( ♯ ‘ { 0 , 1 , 2 } ) = 3 ∧ ( { 𝑥 , 𝑦 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑥 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ∧ { 𝑦 , 𝑧 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 0 , 2 } , { 1 , 2 } } ∪ { { 3 , 4 } , { 3 , 5 } , { 4 , 5 } } ) ) ) ) )
81 75 80 mpbir ⊢ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐺 )