Proof of Theorem usgrexmpl1lem
Step | Hyp | Ref
| Expression |
1 | | prex 5455 |
. . . . 5
⊢ {0, 1}
∈ V |
2 | | prex 5455 |
. . . . 5
⊢ {0, 2}
∈ V |
3 | | prex 5455 |
. . . . 5
⊢ {1, 2}
∈ V |
4 | 1, 2, 3 | 3pm3.2i 1339 |
. . . 4
⊢ ({0, 1}
∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) |
5 | | prex 5455 |
. . . 4
⊢ {0, 3}
∈ V |
6 | | prex 5455 |
. . . . 5
⊢ {3, 4}
∈ V |
7 | | prex 5455 |
. . . . 5
⊢ {3, 5}
∈ V |
8 | | prex 5455 |
. . . . 5
⊢ {4, 5}
∈ V |
9 | 6, 7, 8 | 3pm3.2i 1339 |
. . . 4
⊢ ({3, 4}
∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V) |
10 | 4, 5, 9 | 3pm3.2i 1339 |
. . 3
⊢ (({0, 1}
∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈
V)) |
11 | | 0nn0 12564 |
. . . . . . . . . 10
⊢ 0 ∈
ℕ0 |
12 | | 1nn0 12565 |
. . . . . . . . . 10
⊢ 1 ∈
ℕ0 |
13 | 11, 12 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 ∧ 1 ∈ ℕ0) |
14 | | 2nn0 12566 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ0 |
15 | 11, 14 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 ∧ 2 ∈ ℕ0) |
16 | 13, 15 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 2 ∈ ℕ0)) |
17 | | ax-1ne0 11249 |
. . . . . . . . . 10
⊢ 1 ≠
0 |
18 | | 1ne2 12497 |
. . . . . . . . . 10
⊢ 1 ≠
2 |
19 | 17, 18 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ≠ 0
∧ 1 ≠ 2) |
20 | 19 | olci 865 |
. . . . . . . 8
⊢ ((0 ≠
0 ∧ 0 ≠ 2) ∨ (1 ≠ 0 ∧ 1 ≠ 2)) |
21 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 2 ∈ ℕ0)) → (((0 ≠ 0
∧ 0 ≠ 2) ∨ (1 ≠ 0 ∧ 1 ≠ 2)) → {0, 1} ≠ {0,
2})) |
22 | 16, 20, 21 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {0, 2} |
23 | 12, 14 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ∈
ℕ0 ∧ 2 ∈ ℕ0) |
24 | 13, 23 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (1 ∈
ℕ0 ∧ 2 ∈ ℕ0)) |
25 | | 0ne1 12360 |
. . . . . . . . . 10
⊢ 0 ≠
1 |
26 | | 0ne2 12496 |
. . . . . . . . . 10
⊢ 0 ≠
2 |
27 | 25, 26 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ≠ 1
∧ 0 ≠ 2) |
28 | 27 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2)) |
29 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (1 ∈
ℕ0 ∧ 2 ∈ ℕ0)) → (((0 ≠ 1
∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2)) → {0, 1} ≠ {1,
2})) |
30 | 24, 28, 29 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {1, 2} |
31 | | 3nn0 12567 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
32 | 11, 31 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0) |
33 | 13, 32 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) |
34 | | 1re 11286 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
35 | | 1lt3 12462 |
. . . . . . . . . . 11
⊢ 1 <
3 |
36 | 34, 35 | ltneii 11399 |
. . . . . . . . . 10
⊢ 1 ≠
3 |
37 | 17, 36 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ≠ 0
∧ 1 ≠ 3) |
38 | 37 | olci 865 |
. . . . . . . 8
⊢ ((0 ≠
0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3)) |
39 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) → (((0 ≠ 0
∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3)) → {0, 1} ≠ {0,
3})) |
40 | 33, 38, 39 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {0, 3} |
41 | 22, 30, 40 | 3pm3.2i 1339 |
. . . . . 6
⊢ ({0, 1}
≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) |
42 | | 4nn0 12568 |
. . . . . . . . . 10
⊢ 4 ∈
ℕ0 |
43 | 31, 42 | pm3.2i 470 |
. . . . . . . . 9
⊢ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0) |
44 | 13, 43 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) |
45 | | 0re 11288 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
46 | | 3pos 12394 |
. . . . . . . . . . 11
⊢ 0 <
3 |
47 | 45, 46 | ltneii 11399 |
. . . . . . . . . 10
⊢ 0 ≠
3 |
48 | | 4pos 12396 |
. . . . . . . . . . 11
⊢ 0 <
4 |
49 | 45, 48 | ltneii 11399 |
. . . . . . . . . 10
⊢ 0 ≠
4 |
50 | 47, 49 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ≠ 3
∧ 0 ≠ 4) |
51 | 50 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4)) |
52 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4)) → {0, 1} ≠ {3,
4})) |
53 | 44, 51, 52 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {3, 4} |
54 | | 5nn0 12569 |
. . . . . . . . . 10
⊢ 5 ∈
ℕ0 |
55 | 31, 54 | pm3.2i 470 |
. . . . . . . . 9
⊢ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0) |
56 | 13, 55 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
57 | | 5pos 12398 |
. . . . . . . . . . 11
⊢ 0 <
5 |
58 | 45, 57 | ltneii 11399 |
. . . . . . . . . 10
⊢ 0 ≠
5 |
59 | 47, 58 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ≠ 3
∧ 0 ≠ 5) |
60 | 59 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
3 ∧ 0 ≠ 5) ∨ (1 ≠ 3 ∧ 1 ≠ 5)) |
61 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 5) ∨ (1 ≠ 3 ∧ 1 ≠ 5)) → {0, 1} ≠ {3,
5})) |
62 | 56, 60, 61 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {3, 5} |
63 | 42, 54 | pm3.2i 470 |
. . . . . . . . 9
⊢ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0) |
64 | 13, 63 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
65 | 49, 58 | pm3.2i 470 |
. . . . . . . . 9
⊢ (0 ≠ 4
∧ 0 ≠ 5) |
66 | 65 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5)) |
67 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 4
∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5)) → {0, 1} ≠ {4,
5})) |
68 | 64, 66, 67 | mp2 9 |
. . . . . . 7
⊢ {0, 1}
≠ {4, 5} |
69 | 53, 62, 68 | 3pm3.2i 1339 |
. . . . . 6
⊢ ({0, 1}
≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5}) |
70 | 41, 69 | pm3.2i 470 |
. . . . 5
⊢ (({0, 1}
≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧ ({0, 1}
≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4,
5})) |
71 | 15, 23 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (1 ∈
ℕ0 ∧ 2 ∈ ℕ0)) |
72 | 27 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
1 ∧ 0 ≠ 2) ∨ (2 ≠ 1 ∧ 2 ≠ 2)) |
73 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (1 ∈
ℕ0 ∧ 2 ∈ ℕ0)) → (((0 ≠ 1
∧ 0 ≠ 2) ∨ (2 ≠ 1 ∧ 2 ≠ 2)) → {0, 2} ≠ {1,
2})) |
74 | 71, 72, 73 | mp2 9 |
. . . . . . 7
⊢ {0, 2}
≠ {1, 2} |
75 | 15, 32 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) |
76 | | 2ne0 12393 |
. . . . . . . . . 10
⊢ 2 ≠
0 |
77 | | 2re 12363 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
78 | | 2lt3 12461 |
. . . . . . . . . . 11
⊢ 2 <
3 |
79 | 77, 78 | ltneii 11399 |
. . . . . . . . . 10
⊢ 2 ≠
3 |
80 | 76, 79 | pm3.2i 470 |
. . . . . . . . 9
⊢ (2 ≠ 0
∧ 2 ≠ 3) |
81 | 80 | olci 865 |
. . . . . . . 8
⊢ ((0 ≠
0 ∧ 0 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) |
82 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) → (((0 ≠ 0
∧ 0 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) → {0, 2} ≠ {0,
3})) |
83 | 75, 81, 82 | mp2 9 |
. . . . . . 7
⊢ {0, 2}
≠ {0, 3} |
84 | 74, 83 | pm3.2i 470 |
. . . . . 6
⊢ ({0, 2}
≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) |
85 | 15, 43 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) |
86 | 50 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
3 ∧ 0 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) |
87 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) → {0, 2} ≠ {3,
4})) |
88 | 85, 86, 87 | mp2 9 |
. . . . . . 7
⊢ {0, 2}
≠ {3, 4} |
89 | 15, 55 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
90 | 59 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
3 ∧ 0 ≠ 5) ∨ (2 ≠ 3 ∧ 2 ≠ 5)) |
91 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 5) ∨ (2 ≠ 3 ∧ 2 ≠ 5)) → {0, 2} ≠ {3,
5})) |
92 | 89, 90, 91 | mp2 9 |
. . . . . . 7
⊢ {0, 2}
≠ {3, 5} |
93 | 15, 63 | pm3.2i 470 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
94 | 65 | orci 864 |
. . . . . . . 8
⊢ ((0 ≠
4 ∧ 0 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) |
95 | | prneimg 4879 |
. . . . . . . 8
⊢ (((0
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 4
∧ 0 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) → {0, 2} ≠ {4,
5})) |
96 | 93, 94, 95 | mp2 9 |
. . . . . . 7
⊢ {0, 2}
≠ {4, 5} |
97 | 88, 92, 96 | 3pm3.2i 1339 |
. . . . . 6
⊢ ({0, 2}
≠ {3, 4} ∧ {0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5}) |
98 | 84, 97 | pm3.2i 470 |
. . . . 5
⊢ (({0, 2}
≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧ {0, 2}
≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) |
99 | 23, 32 | pm3.2i 470 |
. . . . . . 7
⊢ ((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) |
100 | 37 | orci 864 |
. . . . . . 7
⊢ ((1 ≠
0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) |
101 | | prneimg 4879 |
. . . . . . 7
⊢ (((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈
ℕ0 ∧ 3 ∈ ℕ0)) → (((1 ≠ 0
∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) → {1, 2} ≠ {0,
3})) |
102 | 99, 100, 101 | mp2 9 |
. . . . . 6
⊢ {1, 2}
≠ {0, 3} |
103 | 23, 43 | pm3.2i 470 |
. . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) |
104 | | 1lt4 12465 |
. . . . . . . . . . 11
⊢ 1 <
4 |
105 | 34, 104 | ltneii 11399 |
. . . . . . . . . 10
⊢ 1 ≠
4 |
106 | 36, 105 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ≠ 3
∧ 1 ≠ 4) |
107 | 106 | orci 864 |
. . . . . . . 8
⊢ ((1 ≠
3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) |
108 | | prneimg 4879 |
. . . . . . . 8
⊢ (((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) → (((1 ≠ 3
∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) → {1, 2} ≠ {3,
4})) |
109 | 103, 107,
108 | mp2 9 |
. . . . . . 7
⊢ {1, 2}
≠ {3, 4} |
110 | 23, 55 | pm3.2i 470 |
. . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
111 | | 1lt5 12469 |
. . . . . . . . . . 11
⊢ 1 <
5 |
112 | 34, 111 | ltneii 11399 |
. . . . . . . . . 10
⊢ 1 ≠
5 |
113 | 36, 112 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ≠ 3
∧ 1 ≠ 5) |
114 | 113 | orci 864 |
. . . . . . . 8
⊢ ((1 ≠
3 ∧ 1 ≠ 5) ∨ (2 ≠ 3 ∧ 2 ≠ 5)) |
115 | | prneimg 4879 |
. . . . . . . 8
⊢ (((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((1 ≠ 3
∧ 1 ≠ 5) ∨ (2 ≠ 3 ∧ 2 ≠ 5)) → {1, 2} ≠ {3,
5})) |
116 | 110, 114,
115 | mp2 9 |
. . . . . . 7
⊢ {1, 2}
≠ {3, 5} |
117 | 23, 63 | pm3.2i 470 |
. . . . . . . 8
⊢ ((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
118 | 105, 112 | pm3.2i 470 |
. . . . . . . . 9
⊢ (1 ≠ 4
∧ 1 ≠ 5) |
119 | 118 | orci 864 |
. . . . . . . 8
⊢ ((1 ≠
4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) |
120 | | prneimg 4879 |
. . . . . . . 8
⊢ (((1
∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((1 ≠ 4
∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) → {1, 2} ≠ {4,
5})) |
121 | 117, 119,
120 | mp2 9 |
. . . . . . 7
⊢ {1, 2}
≠ {4, 5} |
122 | 109, 116,
121 | 3pm3.2i 1339 |
. . . . . 6
⊢ ({1, 2}
≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}) |
123 | 102, 122 | pm3.2i 470 |
. . . . 5
⊢ ({1, 2}
≠ {0, 3} ∧ ({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2}
≠ {4, 5})) |
124 | 70, 98, 123 | 3pm3.2i 1339 |
. . . 4
⊢ ((({0, 1}
≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧ ({0, 1}
≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧ (({0, 2}
≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧ {0, 2}
≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧ ({1, 2}
≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4,
5}))) |
125 | 32, 43 | pm3.2i 470 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) |
126 | 50 | orci 864 |
. . . . . . 7
⊢ ((0 ≠
3 ∧ 0 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4)) |
127 | | prneimg 4879 |
. . . . . . 7
⊢ (((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 4 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4)) → {0, 3} ≠ {3,
4})) |
128 | 125, 126,
127 | mp2 9 |
. . . . . 6
⊢ {0, 3}
≠ {3, 4} |
129 | 32, 55 | pm3.2i 470 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
130 | 59 | orci 864 |
. . . . . . 7
⊢ ((0 ≠
3 ∧ 0 ≠ 5) ∨ (3 ≠ 3 ∧ 3 ≠ 5)) |
131 | | prneimg 4879 |
. . . . . . 7
⊢ (((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 3
∧ 0 ≠ 5) ∨ (3 ≠ 3 ∧ 3 ≠ 5)) → {0, 3} ≠ {3,
5})) |
132 | 129, 130,
131 | mp2 9 |
. . . . . 6
⊢ {0, 3}
≠ {3, 5} |
133 | 32, 63 | pm3.2i 470 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
134 | 65 | orci 864 |
. . . . . . 7
⊢ ((0 ≠
4 ∧ 0 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5)) |
135 | | prneimg 4879 |
. . . . . . 7
⊢ (((0
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 4
∧ 0 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5)) → {0, 3} ≠ {4,
5})) |
136 | 133, 134,
135 | mp2 9 |
. . . . . 6
⊢ {0, 3}
≠ {4, 5} |
137 | 128, 132,
136 | 3pm3.2i 1339 |
. . . . 5
⊢ ({0, 3}
≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) |
138 | 43, 55 | pm3.2i 470 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
139 | | 3re 12369 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
140 | | 3lt4 12463 |
. . . . . . . . . . 11
⊢ 3 <
4 |
141 | 139, 140 | ltneii 11399 |
. . . . . . . . . 10
⊢ 3 ≠
4 |
142 | 141 | necomi 2997 |
. . . . . . . . 9
⊢ 4 ≠
3 |
143 | | 4re 12373 |
. . . . . . . . . 10
⊢ 4 ∈
ℝ |
144 | | 4lt5 12466 |
. . . . . . . . . 10
⊢ 4 <
5 |
145 | 143, 144 | ltneii 11399 |
. . . . . . . . 9
⊢ 4 ≠
5 |
146 | 142, 145 | pm3.2i 470 |
. . . . . . . 8
⊢ (4 ≠ 3
∧ 4 ≠ 5) |
147 | 146 | olci 865 |
. . . . . . 7
⊢ ((3 ≠
3 ∧ 3 ≠ 5) ∨ (4 ≠ 3 ∧ 4 ≠ 5)) |
148 | | prneimg 4879 |
. . . . . . 7
⊢ (((3
∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (3 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((3 ≠ 3
∧ 3 ≠ 5) ∨ (4 ≠ 3 ∧ 4 ≠ 5)) → {3, 4} ≠ {3,
5})) |
149 | 138, 147,
148 | mp2 9 |
. . . . . 6
⊢ {3, 4}
≠ {3, 5} |
150 | 43, 63 | pm3.2i 470 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
151 | | 3lt5 12467 |
. . . . . . . . . 10
⊢ 3 <
5 |
152 | 139, 151 | ltneii 11399 |
. . . . . . . . 9
⊢ 3 ≠
5 |
153 | 141, 152 | pm3.2i 470 |
. . . . . . . 8
⊢ (3 ≠ 4
∧ 3 ≠ 5) |
154 | 153 | orci 864 |
. . . . . . 7
⊢ ((3 ≠
4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5)) |
155 | | prneimg 4879 |
. . . . . . 7
⊢ (((3
∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((3 ≠ 4
∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5)) → {3, 4} ≠ {4,
5})) |
156 | 150, 154,
155 | mp2 9 |
. . . . . 6
⊢ {3, 4}
≠ {4, 5} |
157 | 55, 63 | pm3.2i 470 |
. . . . . . 7
⊢ ((3
∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) |
158 | 153 | orci 864 |
. . . . . . 7
⊢ ((3 ≠
4 ∧ 3 ≠ 5) ∨ (5 ≠ 4 ∧ 5 ≠ 5)) |
159 | | prneimg 4879 |
. . . . . . 7
⊢ (((3
∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (4 ∈
ℕ0 ∧ 5 ∈ ℕ0)) → (((3 ≠ 4
∧ 3 ≠ 5) ∨ (5 ≠ 4 ∧ 5 ≠ 5)) → {3, 5} ≠ {4,
5})) |
160 | 157, 158,
159 | mp2 9 |
. . . . . 6
⊢ {3, 5}
≠ {4, 5} |
161 | 149, 156,
160 | 3pm3.2i 1339 |
. . . . 5
⊢ ({3, 4}
≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5}) |
162 | 137, 161 | pm3.2i 470 |
. . . 4
⊢ (({0, 3}
≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧ ({3, 4}
≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4,
5})) |
163 | 124, 162 | pm3.2i 470 |
. . 3
⊢ (((({0,
1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧ ({0, 1}
≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧ (({0, 2}
≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧ {0, 2}
≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧ ({1, 2}
≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧ (({0, 3}
≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧ ({3, 4}
≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4,
5}))) |
164 | 10, 163 | pm3.2i 470 |
. 2
⊢ ((({0, 1}
∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4,
5})))) |
165 | | usgrexmpl1.e |
. 2
⊢ 𝐸 = 〈“{0, 1} {0, 2}
{1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 |
166 | | s7f1o 15011 |
. . . . . . 7
⊢ (((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5}))))
→ (𝐸 =
〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉
→ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}))) |
167 | 166 | imp 406 |
. . . . . 6
⊢ ((((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})))) ∧
𝐸 = 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉) → 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
168 | | s7len 14947 |
. . . . . . . 8
⊢
(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5}
{4, 5}”〉) = 7 |
169 | 168 | oveq2i 7456 |
. . . . . . 7
⊢
(0..^(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3,
5} {4, 5}”〉)) = (0..^7) |
170 | | f1oeq2 6850 |
. . . . . . 7
⊢
((0..^(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3,
5} {4, 5}”〉)) = (0..^7) → (𝐸:(0..^(♯‘〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}))) |
171 | 169, 170 | ax-mp 5 |
. . . . . 6
⊢ (𝐸:(0..^(♯‘〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
172 | 167, 171 | sylibr 234 |
. . . . 5
⊢ ((((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})))) ∧
𝐸 = 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉) → 𝐸:(0..^(♯‘〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
173 | 165 | dmeqi 5928 |
. . . . . . 7
⊢ dom 𝐸 = dom 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 |
174 | | s7cli 14930 |
. . . . . . . 8
⊢
〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4,
5}”〉 ∈ Word V |
175 | | wrddm 14565 |
. . . . . . . 8
⊢
(〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4,
5}”〉 ∈ Word V → dom 〈“{0, 1} {0, 2} {1, 2} {0,
3} {3, 4} {3, 5} {4, 5}”〉 = (0..^(♯‘〈“{0, 1}
{0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))) |
176 | 174, 175 | ax-mp 5 |
. . . . . . 7
⊢ dom
〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉 =
(0..^(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4,
5}”〉)) |
177 | 173, 176 | eqtri 2762 |
. . . . . 6
⊢ dom 𝐸 =
(0..^(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4,
5}”〉)) |
178 | | f1oeq2 6850 |
. . . . . 6
⊢ (dom
𝐸 =
(0..^(♯‘〈“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4,
5}”〉)) → (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) ↔ 𝐸:(0..^(♯‘〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}))) |
179 | 177, 178 | ax-mp 5 |
. . . . 5
⊢ (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) ↔ 𝐸:(0..^(♯‘〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉))–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
180 | 172, 179 | sylibr 234 |
. . . 4
⊢ ((((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})))) ∧
𝐸 = 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉) → 𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
181 | | f1of1 6860 |
. . . 4
⊢ (𝐸:dom 𝐸–1-1-onto→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) → 𝐸:dom 𝐸–1-1→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
182 | 180, 181 | syl 17 |
. . 3
⊢ ((((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})))) ∧
𝐸 = 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉) → 𝐸:dom 𝐸–1-1→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}})) |
183 | | 0elfz 13677 |
. . . . . . . . . . 11
⊢ (5 ∈
ℕ0 → 0 ∈ (0...5)) |
184 | 54, 183 | ax-mp 5 |
. . . . . . . . . 10
⊢ 0 ∈
(0...5) |
185 | | 5re 12376 |
. . . . . . . . . . . 12
⊢ 5 ∈
ℝ |
186 | 34, 185, 111 | ltleii 11409 |
. . . . . . . . . . 11
⊢ 1 ≤
5 |
187 | | elfz2nn0 13671 |
. . . . . . . . . . 11
⊢ (1 ∈
(0...5) ↔ (1 ∈ ℕ0 ∧ 5 ∈ ℕ0
∧ 1 ≤ 5)) |
188 | 12, 54, 186, 187 | mpbir3an 1341 |
. . . . . . . . . 10
⊢ 1 ∈
(0...5) |
189 | | prssi 4846 |
. . . . . . . . . 10
⊢ ((0
∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆
(0...5)) |
190 | 184, 188,
189 | mp2an 691 |
. . . . . . . . 9
⊢ {0, 1}
⊆ (0...5) |
191 | | 2lt5 12468 |
. . . . . . . . . . . 12
⊢ 2 <
5 |
192 | 77, 185, 191 | ltleii 11409 |
. . . . . . . . . . 11
⊢ 2 ≤
5 |
193 | | elfz2nn0 13671 |
. . . . . . . . . . 11
⊢ (2 ∈
(0...5) ↔ (2 ∈ ℕ0 ∧ 5 ∈ ℕ0
∧ 2 ≤ 5)) |
194 | 14, 54, 192, 193 | mpbir3an 1341 |
. . . . . . . . . 10
⊢ 2 ∈
(0...5) |
195 | | prssi 4846 |
. . . . . . . . . 10
⊢ ((0
∈ (0...5) ∧ 2 ∈ (0...5)) → {0, 2} ⊆
(0...5)) |
196 | 184, 194,
195 | mp2an 691 |
. . . . . . . . 9
⊢ {0, 2}
⊆ (0...5) |
197 | | prssi 4846 |
. . . . . . . . . 10
⊢ ((1
∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆
(0...5)) |
198 | 188, 194,
197 | mp2an 691 |
. . . . . . . . 9
⊢ {1, 2}
⊆ (0...5) |
199 | | sseq1 4028 |
. . . . . . . . . . 11
⊢ (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1}
⊆ (0...5))) |
200 | | sseq1 4028 |
. . . . . . . . . . 11
⊢ (𝑒 = {0, 2} → (𝑒 ⊆ (0...5) ↔ {0, 2}
⊆ (0...5))) |
201 | | sseq1 4028 |
. . . . . . . . . . 11
⊢ (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2}
⊆ (0...5))) |
202 | 199, 200,
201 | raltpg 4723 |
. . . . . . . . . 10
⊢ (({0, 1}
∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) → (∀𝑒 ∈ {{0, 1}, {0, 2}, {1,
2}}𝑒 ⊆ (0...5) ↔
({0, 1} ⊆ (0...5) ∧ {0, 2} ⊆ (0...5) ∧ {1, 2} ⊆
(0...5)))) |
203 | 4, 202 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
{{0, 1}, {0, 2}, {1, 2}}𝑒
⊆ (0...5) ↔ ({0, 1} ⊆ (0...5) ∧ {0, 2} ⊆ (0...5)
∧ {1, 2} ⊆ (0...5))) |
204 | 190, 196,
198, 203 | mpbir3an 1341 |
. . . . . . . 8
⊢
∀𝑒 ∈
{{0, 1}, {0, 2}, {1, 2}}𝑒
⊆ (0...5) |
205 | 139, 185,
151 | ltleii 11409 |
. . . . . . . . . . 11
⊢ 3 ≤
5 |
206 | | elfz2nn0 13671 |
. . . . . . . . . . 11
⊢ (3 ∈
(0...5) ↔ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0
∧ 3 ≤ 5)) |
207 | 31, 54, 205, 206 | mpbir3an 1341 |
. . . . . . . . . 10
⊢ 3 ∈
(0...5) |
208 | | prssi 4846 |
. . . . . . . . . 10
⊢ ((0
∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆
(0...5)) |
209 | 184, 207,
208 | mp2an 691 |
. . . . . . . . 9
⊢ {0, 3}
⊆ (0...5) |
210 | | sseq1 4028 |
. . . . . . . . . 10
⊢ (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3}
⊆ (0...5))) |
211 | 5, 210 | ralsn 4705 |
. . . . . . . . 9
⊢
(∀𝑒 ∈
{{0, 3}}𝑒 ⊆ (0...5)
↔ {0, 3} ⊆ (0...5)) |
212 | 209, 211 | mpbir 231 |
. . . . . . . 8
⊢
∀𝑒 ∈
{{0, 3}}𝑒 ⊆
(0...5) |
213 | | ralunb 4214 |
. . . . . . . 8
⊢
(∀𝑒 ∈
({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ {{0, 1}, {0, 2}, {1,
2}}𝑒 ⊆ (0...5) ∧
∀𝑒 ∈ {{0,
3}}𝑒 ⊆
(0...5))) |
214 | 204, 212,
213 | mpbir2an 710 |
. . . . . . 7
⊢
∀𝑒 ∈
({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})𝑒 ⊆ (0...5) |
215 | 143, 185,
144 | ltleii 11409 |
. . . . . . . . . 10
⊢ 4 ≤
5 |
216 | | elfz2nn0 13671 |
. . . . . . . . . 10
⊢ (4 ∈
(0...5) ↔ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0
∧ 4 ≤ 5)) |
217 | 42, 54, 215, 216 | mpbir3an 1341 |
. . . . . . . . 9
⊢ 4 ∈
(0...5) |
218 | | prssi 4846 |
. . . . . . . . 9
⊢ ((3
∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆
(0...5)) |
219 | 207, 217,
218 | mp2an 691 |
. . . . . . . 8
⊢ {3, 4}
⊆ (0...5) |
220 | | nn0fz0 13678 |
. . . . . . . . . 10
⊢ (5 ∈
ℕ0 ↔ 5 ∈ (0...5)) |
221 | 54, 220 | mpbi 230 |
. . . . . . . . 9
⊢ 5 ∈
(0...5) |
222 | | prssi 4846 |
. . . . . . . . 9
⊢ ((3
∈ (0...5) ∧ 5 ∈ (0...5)) → {3, 5} ⊆
(0...5)) |
223 | 207, 221,
222 | mp2an 691 |
. . . . . . . 8
⊢ {3, 5}
⊆ (0...5) |
224 | | prssi 4846 |
. . . . . . . . 9
⊢ ((4
∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆
(0...5)) |
225 | 217, 221,
224 | mp2an 691 |
. . . . . . . 8
⊢ {4, 5}
⊆ (0...5) |
226 | | sseq1 4028 |
. . . . . . . . . 10
⊢ (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4}
⊆ (0...5))) |
227 | | sseq1 4028 |
. . . . . . . . . 10
⊢ (𝑒 = {3, 5} → (𝑒 ⊆ (0...5) ↔ {3, 5}
⊆ (0...5))) |
228 | | sseq1 4028 |
. . . . . . . . . 10
⊢ (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5}
⊆ (0...5))) |
229 | 226, 227,
228 | raltpg 4723 |
. . . . . . . . 9
⊢ (({3, 4}
∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V) → (∀𝑒 ∈ {{3, 4}, {3, 5}, {4,
5}}𝑒 ⊆ (0...5) ↔
({3, 4} ⊆ (0...5) ∧ {3, 5} ⊆ (0...5) ∧ {4, 5} ⊆
(0...5)))) |
230 | 9, 229 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑒 ∈
{{3, 4}, {3, 5}, {4, 5}}𝑒
⊆ (0...5) ↔ ({3, 4} ⊆ (0...5) ∧ {3, 5} ⊆ (0...5)
∧ {4, 5} ⊆ (0...5))) |
231 | 219, 223,
225, 230 | mpbir3an 1341 |
. . . . . . 7
⊢
∀𝑒 ∈
{{3, 4}, {3, 5}, {4, 5}}𝑒
⊆ (0...5) |
232 | | ralunb 4214 |
. . . . . . 7
⊢
(∀𝑒 ∈
(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})𝑒 ⊆ (0...5) ↔
(∀𝑒 ∈ ({{0, 1},
{0, 2}, {1, 2}} ∪ {{0, 3}})𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{3, 4}, {3, 5}, {4,
5}}𝑒 ⊆
(0...5))) |
233 | 214, 231,
232 | mpbir2an 710 |
. . . . . 6
⊢
∀𝑒 ∈
(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})𝑒 ⊆
(0...5) |
234 | | pwssb 5127 |
. . . . . 6
⊢ ((({{0,
1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆
𝒫 (0...5) ↔ ∀𝑒 ∈ (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0,
3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})𝑒 ⊆ (0...5)) |
235 | 233, 234 | mpbir 231 |
. . . . 5
⊢ (({{0,
1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆
𝒫 (0...5) |
236 | | usgrexmpl1.v |
. . . . . 6
⊢ 𝑉 = (0...5) |
237 | 236 | pweqi 4638 |
. . . . 5
⊢ 𝒫
𝑉 = 𝒫
(0...5) |
238 | 235, 237 | sseqtrri 4040 |
. . . 4
⊢ (({{0,
1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆
𝒫 𝑉 |
239 | | prhash2ex 14444 |
. . . . . . 7
⊢
(♯‘{0, 1}) = 2 |
240 | | c0ex 11280 |
. . . . . . . . 9
⊢ 0 ∈
V |
241 | | 2ex 12366 |
. . . . . . . . 9
⊢ 2 ∈
V |
242 | 240, 241,
26 | 3pm3.2i 1339 |
. . . . . . . 8
⊢ (0 ∈
V ∧ 2 ∈ V ∧ 0 ≠ 2) |
243 | | hashprb 14442 |
. . . . . . . 8
⊢ ((0
∈ V ∧ 2 ∈ V ∧ 0 ≠ 2) ↔ (♯‘{0, 2}) =
2) |
244 | 242, 243 | mpbi 230 |
. . . . . . 7
⊢
(♯‘{0, 2}) = 2 |
245 | | 1ex 11282 |
. . . . . . . . 9
⊢ 1 ∈
V |
246 | 245, 241,
18 | 3pm3.2i 1339 |
. . . . . . . 8
⊢ (1 ∈
V ∧ 2 ∈ V ∧ 1 ≠ 2) |
247 | | hashprb 14442 |
. . . . . . . 8
⊢ ((1
∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) =
2) |
248 | 246, 247 | mpbi 230 |
. . . . . . 7
⊢
(♯‘{1, 2}) = 2 |
249 | | fveqeq2 6928 |
. . . . . . . . 9
⊢ (𝑒 = {0, 1} →
((♯‘𝑒) = 2
↔ (♯‘{0, 1}) = 2)) |
250 | | fveqeq2 6928 |
. . . . . . . . 9
⊢ (𝑒 = {0, 2} →
((♯‘𝑒) = 2
↔ (♯‘{0, 2}) = 2)) |
251 | | fveqeq2 6928 |
. . . . . . . . 9
⊢ (𝑒 = {1, 2} →
((♯‘𝑒) = 2
↔ (♯‘{1, 2}) = 2)) |
252 | 249, 250,
251 | raltpg 4723 |
. . . . . . . 8
⊢ (({0, 1}
∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) → (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}}
(♯‘𝑒) = 2
↔ ((♯‘{0, 1}) = 2 ∧ (♯‘{0, 2}) = 2 ∧
(♯‘{1, 2}) = 2))) |
253 | 4, 252 | ax-mp 5 |
. . . . . . 7
⊢
(∀𝑒 ∈
{{0, 1}, {0, 2}, {1, 2}} (♯‘𝑒) = 2 ↔ ((♯‘{0, 1}) = 2
∧ (♯‘{0, 2}) = 2 ∧ (♯‘{1, 2}) =
2)) |
254 | 239, 244,
248, 253 | mpbir3an 1341 |
. . . . . 6
⊢
∀𝑒 ∈
{{0, 1}, {0, 2}, {1, 2}} (♯‘𝑒) = 2 |
255 | | 3ex 12371 |
. . . . . . . . 9
⊢ 3 ∈
V |
256 | 240, 255,
47 | 3pm3.2i 1339 |
. . . . . . . 8
⊢ (0 ∈
V ∧ 3 ∈ V ∧ 0 ≠ 3) |
257 | | hashprb 14442 |
. . . . . . . 8
⊢ ((0
∈ V ∧ 3 ∈ V ∧ 0 ≠ 3) ↔ (♯‘{0, 3}) =
2) |
258 | 256, 257 | mpbi 230 |
. . . . . . 7
⊢
(♯‘{0, 3}) = 2 |
259 | | fveqeq2 6928 |
. . . . . . . 8
⊢ (𝑒 = {0, 3} →
((♯‘𝑒) = 2
↔ (♯‘{0, 3}) = 2)) |
260 | 5, 259 | ralsn 4705 |
. . . . . . 7
⊢
(∀𝑒 ∈
{{0, 3}} (♯‘𝑒)
= 2 ↔ (♯‘{0, 3}) = 2) |
261 | 258, 260 | mpbir 231 |
. . . . . 6
⊢
∀𝑒 ∈
{{0, 3}} (♯‘𝑒)
= 2 |
262 | | ralunb 4214 |
. . . . . 6
⊢
(∀𝑒 ∈
({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}}
(♯‘𝑒) = 2 ∧
∀𝑒 ∈ {{0, 3}}
(♯‘𝑒) =
2)) |
263 | 254, 261,
262 | mpbir2an 710 |
. . . . 5
⊢
∀𝑒 ∈
({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})(♯‘𝑒) = 2 |
264 | 143 | elexi 3506 |
. . . . . . . 8
⊢ 4 ∈
V |
265 | 255, 264,
141 | 3pm3.2i 1339 |
. . . . . . 7
⊢ (3 ∈
V ∧ 4 ∈ V ∧ 3 ≠ 4) |
266 | | hashprb 14442 |
. . . . . . 7
⊢ ((3
∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) =
2) |
267 | 265, 266 | mpbi 230 |
. . . . . 6
⊢
(♯‘{3, 4}) = 2 |
268 | 185 | elexi 3506 |
. . . . . . . 8
⊢ 5 ∈
V |
269 | 255, 268,
152 | 3pm3.2i 1339 |
. . . . . . 7
⊢ (3 ∈
V ∧ 5 ∈ V ∧ 3 ≠ 5) |
270 | | hashprb 14442 |
. . . . . . 7
⊢ ((3
∈ V ∧ 5 ∈ V ∧ 3 ≠ 5) ↔ (♯‘{3, 5}) =
2) |
271 | 269, 270 | mpbi 230 |
. . . . . 6
⊢
(♯‘{3, 5}) = 2 |
272 | 264, 268,
145 | 3pm3.2i 1339 |
. . . . . . 7
⊢ (4 ∈
V ∧ 5 ∈ V ∧ 4 ≠ 5) |
273 | | hashprb 14442 |
. . . . . . 7
⊢ ((4
∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) =
2) |
274 | 272, 273 | mpbi 230 |
. . . . . 6
⊢
(♯‘{4, 5}) = 2 |
275 | | fveqeq2 6928 |
. . . . . . . 8
⊢ (𝑒 = {3, 4} →
((♯‘𝑒) = 2
↔ (♯‘{3, 4}) = 2)) |
276 | | fveqeq2 6928 |
. . . . . . . 8
⊢ (𝑒 = {3, 5} →
((♯‘𝑒) = 2
↔ (♯‘{3, 5}) = 2)) |
277 | | fveqeq2 6928 |
. . . . . . . 8
⊢ (𝑒 = {4, 5} →
((♯‘𝑒) = 2
↔ (♯‘{4, 5}) = 2)) |
278 | 275, 276,
277 | raltpg 4723 |
. . . . . . 7
⊢ (({3, 4}
∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V) → (∀𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}}
(♯‘𝑒) = 2
↔ ((♯‘{3, 4}) = 2 ∧ (♯‘{3, 5}) = 2 ∧
(♯‘{4, 5}) = 2))) |
279 | 9, 278 | ax-mp 5 |
. . . . . 6
⊢
(∀𝑒 ∈
{{3, 4}, {3, 5}, {4, 5}} (♯‘𝑒) = 2 ↔ ((♯‘{3, 4}) = 2
∧ (♯‘{3, 5}) = 2 ∧ (♯‘{4, 5}) =
2)) |
280 | 267, 271,
274, 279 | mpbir3an 1341 |
. . . . 5
⊢
∀𝑒 ∈
{{3, 4}, {3, 5}, {4, 5}} (♯‘𝑒) = 2 |
281 | | ralunb 4214 |
. . . . 5
⊢
(∀𝑒 ∈
(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4,
5}})(♯‘𝑒) = 2
↔ (∀𝑒 ∈
({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})(♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}}
(♯‘𝑒) =
2)) |
282 | 263, 280,
281 | mpbir2an 710 |
. . . 4
⊢
∀𝑒 ∈
(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4,
5}})(♯‘𝑒) =
2 |
283 | | ssrab 4090 |
. . . 4
⊢ ((({{0,
1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆
{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ ((({{0, 1}, {0,
2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆ 𝒫
𝑉 ∧ ∀𝑒 ∈ (({{0, 1}, {0, 2}, {1,
2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})(♯‘𝑒) = 2)) |
284 | 238, 282,
283 | mpbir2an 710 |
. . 3
⊢ (({{0,
1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆
{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} |
285 | | f1ss 6821 |
. . 3
⊢ ((𝐸:dom 𝐸–1-1→(({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})
∪ {{3, 4}, {3, 5}, {4, 5}}) ∧ (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0,
3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) → 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) |
286 | 182, 284,
285 | sylancl 585 |
. 2
⊢ ((((({0,
1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V) ∧ {0, 3} ∈ V
∧ ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)) ∧
(((({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3}) ∧
({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})) ∧
(({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧
{0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})) ∧ ({1, 2} ≠ {0, 3} ∧
({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))) ∧
(({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5}) ∧
({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})))) ∧
𝐸 = 〈“{0, 1} {0,
2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”〉) → 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) |
287 | 164, 165,
286 | mp2an 691 |
1
⊢ 𝐸:dom 𝐸–1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} |