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 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 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑦 , 𝑧 } = { 0 , 𝑦 , 𝑧 } )
48 47 eqeq2d ⊢ ( 𝑥 = 0 → ( { 0 , 1 , 2 } = { 𝑥 , 𝑦 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ) )
49 preq1 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑦 } = { 0 , 𝑦 } )
50 49 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 } } ) ) ) )
51 preq1 ⊢ ( 𝑥 = 0 → { 𝑥 , 𝑧 } = { 0 , 𝑧 } )
52 51 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 } } ) ) ) )
53 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 } } ) ) ) )
54 50 52 53 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 } } ) ) ) ) )
55 48 54 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 } } ) ) ) ) ) )
56 tpeq2 ⊢ ( 𝑦 = 1 → { 0 , 𝑦 , 𝑧 } = { 0 , 1 , 𝑧 } )
57 56 eqeq2d ⊢ ( 𝑦 = 1 → ( { 0 , 1 , 2 } = { 0 , 𝑦 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ) )
58 preq2 ⊢ ( 𝑦 = 1 → { 0 , 𝑦 } = { 0 , 1 } )
59 58 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 } } ) ) ) )
60 preq1 ⊢ ( 𝑦 = 1 → { 𝑦 , 𝑧 } = { 1 , 𝑧 } )
61 60 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 } } ) ) ) )
62 59 61 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 } } ) ) ) ) )
63 57 62 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 } } ) ) ) ) ) )
64 tpeq3 ⊢ ( 𝑧 = 2 → { 0 , 1 , 𝑧 } = { 0 , 1 , 2 } )
65 64 eqeq2d ⊢ ( 𝑧 = 2 → ( { 0 , 1 , 2 } = { 0 , 1 , 𝑧 } ↔ { 0 , 1 , 2 } = { 0 , 1 , 2 } ) )
66 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 } } ) ) ) )
67 preq2 ⊢ ( 𝑧 = 2 → { 0 , 𝑧 } = { 0 , 2 } )
68 67 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 } } ) ) ) )
69 preq2 ⊢ ( 𝑧 = 2 → { 1 , 𝑧 } = { 1 , 2 } )
70 69 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 } } ) ) ) )
71 66 68 70 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 } } ) ) ) ) )
72 65 71 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 } } ) ) ) ) ) )
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 } } ) ) ) ) ) → ∃ 𝑥 ∈ ( { 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 } } ) ) ) ) )
74 18 46 73 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 } } ) ) ) )
75 1 2 3 usgrexmpl1vtx ⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
76 75 eqcomi ⊢ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) = ( Vtx ‘ 𝐺 )
77 1 2 3 usgrexmpl1edg ⊢ ( Edg ‘ 𝐺 ) = ( { { 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 ‘ 𝐺 )
79 76 78 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 } } ) ) ) ) )
80 74 79 mpbir ⊢ { 0 , 1 , 2 } ∈ ( GrTriangles ‘ 𝐺 )