Step | Hyp | Ref
| Expression |
1 | | c0ex 11280 |
. . . . . . 7
⊢ 0 ∈
V |
2 | 1 | tpid1 4793 |
. . . . . 6
⊢ 0 ∈
{0, 1, 2} |
3 | 2 | orci 864 |
. . . . 5
⊢ (0 ∈
{0, 1, 2} ∨ 0 ∈ {3, 4, 5}) |
4 | | elun 4170 |
. . . . 5
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (0 ∈ {0, 1, 2} ∨ 0 ∈ {3, 4,
5})) |
5 | 3, 4 | mpbir 231 |
. . . 4
⊢ 0 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
6 | | 1ex 11282 |
. . . . . . 7
⊢ 1 ∈
V |
7 | 6 | tpid2 4795 |
. . . . . 6
⊢ 1 ∈
{0, 1, 2} |
8 | 7 | orci 864 |
. . . . 5
⊢ (1 ∈
{0, 1, 2} ∨ 1 ∈ {3, 4, 5}) |
9 | | elun 4170 |
. . . . 5
⊢ (1 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (1 ∈ {0, 1, 2} ∨ 1 ∈ {3, 4,
5})) |
10 | 8, 9 | mpbir 231 |
. . . 4
⊢ 1 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
11 | | 2ex 12366 |
. . . . . . 7
⊢ 2 ∈
V |
12 | 11 | tpid3 4798 |
. . . . . 6
⊢ 2 ∈
{0, 1, 2} |
13 | 12 | orci 864 |
. . . . 5
⊢ (2 ∈
{0, 1, 2} ∨ 2 ∈ {3, 4, 5}) |
14 | | elun 4170 |
. . . . 5
⊢ (2 ∈
({0, 1, 2} ∪ {3, 4, 5}) ↔ (2 ∈ {0, 1, 2} ∨ 2 ∈ {3, 4,
5})) |
15 | 13, 14 | mpbir 231 |
. . . 4
⊢ 2 ∈
({0, 1, 2} ∪ {3, 4, 5}) |
16 | 5, 10, 15 | 3pm3.2i 1339 |
. . 3
⊢ (0 ∈
({0, 1, 2} ∪ {3, 4, 5}) ∧ 1 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∧ 2
∈ ({0, 1, 2} ∪ {3, 4, 5})) |
17 | | eqid 2734 |
. . . 4
⊢ {0, 1, 2}
= {0, 1, 2} |
18 | | ex-hash 30476 |
. . . 4
⊢
(♯‘{0, 1, 2}) = 3 |
19 | | prex 5455 |
. . . . . . . . . 10
⊢ {0, 1}
∈ V |
20 | 19 | tpid1 4793 |
. . . . . . . . 9
⊢ {0, 1}
∈ {{0, 1}, {0, 2}, {1, 2}} |
21 | 20 | orci 864 |
. . . . . . . 8
⊢ ({0, 1}
∈ {{0, 1}, {0, 2}, {1, 2}} ∨ {0, 1} ∈ {{3, 4}, {3, 5}, {4,
5}}) |
22 | | elun 4170 |
. . . . . . . 8
⊢ ({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}})) |
23 | 21, 22 | mpbir 231 |
. . . . . . 7
⊢ {0, 1}
∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}}) |
24 | 23 | olci 865 |
. . . . . 6
⊢ ({0, 1}
∈ {{0, 3}} ∨ {0, 1} ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3,
5}, {4, 5}})) |
25 | | elun 4170 |
. . . . . 6
⊢ ({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}}))) |
26 | 24, 25 | mpbir 231 |
. . . . 5
⊢ {0, 1}
∈ ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}})) |
27 | | prex 5455 |
. . . . . . . . . 10
⊢ {0, 2}
∈ V |
28 | 27 | tpid2 4795 |
. . . . . . . . 9
⊢ {0, 2}
∈ {{0, 1}, {0, 2}, {1, 2}} |
29 | 28 | orci 864 |
. . . . . . . 8
⊢ ({0, 2}
∈ {{0, 1}, {0, 2}, {1, 2}} ∨ {0, 2} ∈ {{3, 4}, {3, 5}, {4,
5}}) |
30 | | elun 4170 |
. . . . . . . 8
⊢ ({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}})) |
31 | 29, 30 | mpbir 231 |
. . . . . . 7
⊢ {0, 2}
∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}}) |
32 | 31 | olci 865 |
. . . . . 6
⊢ ({0, 2}
∈ {{0, 3}} ∨ {0, 2} ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3,
5}, {4, 5}})) |
33 | | elun 4170 |
. . . . . 6
⊢ ({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}}))) |
34 | 32, 33 | mpbir 231 |
. . . . 5
⊢ {0, 2}
∈ ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}})) |
35 | | prex 5455 |
. . . . . . . . . 10
⊢ {1, 2}
∈ V |
36 | 35 | tpid3 4798 |
. . . . . . . . 9
⊢ {1, 2}
∈ {{0, 1}, {0, 2}, {1, 2}} |
37 | 36 | orci 864 |
. . . . . . . 8
⊢ ({1, 2}
∈ {{0, 1}, {0, 2}, {1, 2}} ∨ {1, 2} ∈ {{3, 4}, {3, 5}, {4,
5}}) |
38 | | elun 4170 |
. . . . . . . 8
⊢ ({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}})) |
39 | 37, 38 | mpbir 231 |
. . . . . . 7
⊢ {1, 2}
∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}}) |
40 | 39 | olci 865 |
. . . . . 6
⊢ ({1, 2}
∈ {{0, 3}} ∨ {1, 2} ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3,
5}, {4, 5}})) |
41 | | elun 4170 |
. . . . . 6
⊢ ({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}}))) |
42 | 40, 41 | mpbir 231 |
. . . . 5
⊢ {1, 2}
∈ ({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}})) |
43 | 26, 34, 42 | 3pm3.2i 1339 |
. . . 4
⊢ ({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}}))) |
44 | 17, 18, 43 | 3pm3.2i 1339 |
. . 3
⊢ ({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}})))) |
45 | | tpeq1 4767 |
. . . . . 6
⊢ (𝑥 = 0 → {𝑥, 𝑦, 𝑧} = {0, 𝑦, 𝑧}) |
46 | 45 | eqeq2d 2745 |
. . . . 5
⊢ (𝑥 = 0 → ({0, 1, 2} = {𝑥, 𝑦, 𝑧} ↔ {0, 1, 2} = {0, 𝑦, 𝑧})) |
47 | | preq1 4758 |
. . . . . . 7
⊢ (𝑥 = 0 → {𝑥, 𝑦} = {0, 𝑦}) |
48 | 47 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 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}})))) |
49 | | preq1 4758 |
. . . . . . 7
⊢ (𝑥 = 0 → {𝑥, 𝑧} = {0, 𝑧}) |
50 | 49 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 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 | | biidd 262 |
. . . . . 6
⊢ (𝑥 = 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}})))) |
52 | 48, 50, 51 | 3anbi123d 1436 |
. . . . 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, 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}}))))) |
53 | 46, 52 | 3anbi13d 1438 |
. . . 4
⊢ (𝑥 = 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}})))))) |
54 | | tpeq2 4768 |
. . . . . 6
⊢ (𝑦 = 1 → {0, 𝑦, 𝑧} = {0, 1, 𝑧}) |
55 | 54 | eqeq2d 2745 |
. . . . 5
⊢ (𝑦 = 1 → ({0, 1, 2} = {0,
𝑦, 𝑧} ↔ {0, 1, 2} = {0, 1, 𝑧})) |
56 | | preq2 4759 |
. . . . . . 7
⊢ (𝑦 = 1 → {0, 𝑦} = {0, 1}) |
57 | 56 | eleq1d 2823 |
. . . . . 6
⊢ (𝑦 = 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}})))) |
58 | | preq1 4758 |
. . . . . . 7
⊢ (𝑦 = 1 → {𝑦, 𝑧} = {1, 𝑧}) |
59 | 58 | eleq1d 2823 |
. . . . . 6
⊢ (𝑦 = 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}})))) |
60 | 57, 59 | 3anbi13d 1438 |
. . . . 5
⊢ (𝑦 = 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}}))))) |
61 | 55, 60 | 3anbi13d 1438 |
. . . 4
⊢ (𝑦 = 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}})))))) |
62 | | tpeq3 4769 |
. . . . . 6
⊢ (𝑧 = 2 → {0, 1, 𝑧} = {0, 1, 2}) |
63 | 62 | eqeq2d 2745 |
. . . . 5
⊢ (𝑧 = 2 → ({0, 1, 2} = {0, 1,
𝑧} ↔ {0, 1, 2} = {0,
1, 2})) |
64 | | biidd 262 |
. . . . . 6
⊢ (𝑧 = 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}})))) |
65 | | preq2 4759 |
. . . . . . 7
⊢ (𝑧 = 2 → {0, 𝑧} = {0, 2}) |
66 | 65 | eleq1d 2823 |
. . . . . 6
⊢ (𝑧 = 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}})))) |
67 | | preq2 4759 |
. . . . . . 7
⊢ (𝑧 = 2 → {1, 𝑧} = {1, 2}) |
68 | 67 | eleq1d 2823 |
. . . . . 6
⊢ (𝑧 = 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}})))) |
69 | 64, 66, 68 | 3anbi123d 1436 |
. . . . 5
⊢ (𝑧 = 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}}))))) |
70 | 63, 69 | 3anbi13d 1438 |
. . . 4
⊢ (𝑧 = 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}})))))) |
71 | 53, 61, 70 | rspc3ev 3648 |
. . 3
⊢ (((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}}))))) |
72 | 16, 44, 71 | mp2an 691 |
. 2
⊢
∃𝑥 ∈ ({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}})))) |
73 | | usgrexmpl1.v |
. . . . 5
⊢ 𝑉 = (0...5) |
74 | | usgrexmpl1.e |
. . . . 5
⊢ 𝐸 = 〈“{0, 1} {0, 2}
{1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 |
75 | | usgrexmpl1.g |
. . . . 5
⊢ 𝐺 = 〈𝑉, 𝐸〉 |
76 | 73, 74, 75 | usgrexmpl1vtx 47758 |
. . . 4
⊢
(Vtx‘𝐺) = ({0,
1, 2} ∪ {3, 4, 5}) |
77 | 76 | eqcomi 2743 |
. . 3
⊢ ({0, 1,
2} ∪ {3, 4, 5}) = (Vtx‘𝐺) |
78 | 73, 74, 75 | usgrexmpl1edg 47759 |
. . . 4
⊢
(Edg‘𝐺) =
({{0, 3}} ∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4,
5}})) |
79 | 78 | eqcomi 2743 |
. . 3
⊢ ({{0, 3}}
∪ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{3, 4}, {3, 5}, {4, 5}})) =
(Edg‘𝐺) |
80 | 77, 79 | isgrtri 47724 |
. 2
⊢ ({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 | 72, 80 | mpbir 231 |
1
⊢ {0, 1, 2}
∈ (GrTriangles‘𝐺) |