Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  usgrexmpl1lem Structured version   Visualization version   GIF version

Theorem usgrexmpl1lem 47838
Description: Lemma for usgrexmpl1 47839. (Contributed by AV, 2-Aug-2025.)
Hypotheses
Ref Expression
usgrexmpl1.v 𝑉 = (0...5)
usgrexmpl1.e 𝐸 = ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩
Assertion
Ref Expression
usgrexmpl1lem 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Distinct variable group:   𝑒,𝑉
Allowed substitution hint:   𝐸(𝑒)

Proof of Theorem usgrexmpl1lem
StepHypRef Expression
1 prex 5452 . . . . 5 {0, 1} ∈ V
2 prex 5452 . . . . 5 {0, 2} ∈ V
3 prex 5452 . . . . 5 {1, 2} ∈ V
41, 2, 33pm3.2i 1339 . . . 4 ({0, 1} ∈ V ∧ {0, 2} ∈ V ∧ {1, 2} ∈ V)
5 prex 5452 . . . 4 {0, 3} ∈ V
6 prex 5452 . . . . 5 {3, 4} ∈ V
7 prex 5452 . . . . 5 {3, 5} ∈ V
8 prex 5452 . . . . 5 {4, 5} ∈ V
96, 7, 83pm3.2i 1339 . . . 4 ({3, 4} ∈ V ∧ {3, 5} ∈ V ∧ {4, 5} ∈ V)
104, 5, 93pm3.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 12570 . . . . . . . . . 10 0 ∈ ℕ0
12 1nn0 12571 . . . . . . . . . 10 1 ∈ ℕ0
1311, 12pm3.2i 470 . . . . . . . . 9 (0 ∈ ℕ0 ∧ 1 ∈ ℕ0)
14 2nn0 12572 . . . . . . . . . 10 2 ∈ ℕ0
1511, 14pm3.2i 470 . . . . . . . . 9 (0 ∈ ℕ0 ∧ 2 ∈ ℕ0)
1613, 15pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 2 ∈ ℕ0))
17 ax-1ne0 11255 . . . . . . . . . 10 1 ≠ 0
18 1ne2 12503 . . . . . . . . . 10 1 ≠ 2
1917, 18pm3.2i 470 . . . . . . . . 9 (1 ≠ 0 ∧ 1 ≠ 2)
2019olci 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}))
2216, 20, 21mp2 9 . . . . . . 7 {0, 1} ≠ {0, 2}
2312, 14pm3.2i 470 . . . . . . . . 9 (1 ∈ ℕ0 ∧ 2 ∈ ℕ0)
2413, 23pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (1 ∈ ℕ0 ∧ 2 ∈ ℕ0))
25 0ne1 12366 . . . . . . . . . 10 0 ≠ 1
26 0ne2 12502 . . . . . . . . . 10 0 ≠ 2
2725, 26pm3.2i 470 . . . . . . . . 9 (0 ≠ 1 ∧ 0 ≠ 2)
2827orci 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}))
3024, 28, 29mp2 9 . . . . . . 7 {0, 1} ≠ {1, 2}
31 3nn0 12573 . . . . . . . . . 10 3 ∈ ℕ0
3211, 31pm3.2i 470 . . . . . . . . 9 (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)
3313, 32pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
34 1re 11292 . . . . . . . . . . 11 1 ∈ ℝ
35 1lt3 12468 . . . . . . . . . . 11 1 < 3
3634, 35ltneii 11405 . . . . . . . . . 10 1 ≠ 3
3717, 36pm3.2i 470 . . . . . . . . 9 (1 ≠ 0 ∧ 1 ≠ 3)
3837olci 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}))
4033, 38, 39mp2 9 . . . . . . 7 {0, 1} ≠ {0, 3}
4122, 30, 403pm3.2i 1339 . . . . . 6 ({0, 1} ≠ {0, 2} ∧ {0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {0, 3})
42 4nn0 12574 . . . . . . . . . 10 4 ∈ ℕ0
4331, 42pm3.2i 470 . . . . . . . . 9 (3 ∈ ℕ0 ∧ 4 ∈ ℕ0)
4413, 43pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
45 0re 11294 . . . . . . . . . . 11 0 ∈ ℝ
46 3pos 12400 . . . . . . . . . . 11 0 < 3
4745, 46ltneii 11405 . . . . . . . . . 10 0 ≠ 3
48 4pos 12402 . . . . . . . . . . 11 0 < 4
4945, 48ltneii 11405 . . . . . . . . . 10 0 ≠ 4
5047, 49pm3.2i 470 . . . . . . . . 9 (0 ≠ 3 ∧ 0 ≠ 4)
5150orci 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}))
5344, 51, 52mp2 9 . . . . . . 7 {0, 1} ≠ {3, 4}
54 5nn0 12575 . . . . . . . . . 10 5 ∈ ℕ0
5531, 54pm3.2i 470 . . . . . . . . 9 (3 ∈ ℕ0 ∧ 5 ∈ ℕ0)
5613, 55pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0))
57 5pos 12404 . . . . . . . . . . 11 0 < 5
5845, 57ltneii 11405 . . . . . . . . . 10 0 ≠ 5
5947, 58pm3.2i 470 . . . . . . . . 9 (0 ≠ 3 ∧ 0 ≠ 5)
6059orci 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}))
6256, 60, 61mp2 9 . . . . . . 7 {0, 1} ≠ {3, 5}
6342, 54pm3.2i 470 . . . . . . . . 9 (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)
6413, 63pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
6549, 58pm3.2i 470 . . . . . . . . 9 (0 ≠ 4 ∧ 0 ≠ 5)
6665orci 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}))
6864, 66, 67mp2 9 . . . . . . 7 {0, 1} ≠ {4, 5}
6953, 62, 683pm3.2i 1339 . . . . . 6 ({0, 1} ≠ {3, 4} ∧ {0, 1} ≠ {3, 5} ∧ {0, 1} ≠ {4, 5})
7041, 69pm3.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}))
7115, 23pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (1 ∈ ℕ0 ∧ 2 ∈ ℕ0))
7227orci 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}))
7471, 72, 73mp2 9 . . . . . . 7 {0, 2} ≠ {1, 2}
7515, 32pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
76 2ne0 12399 . . . . . . . . . 10 2 ≠ 0
77 2re 12369 . . . . . . . . . . 11 2 ∈ ℝ
78 2lt3 12467 . . . . . . . . . . 11 2 < 3
7977, 78ltneii 11405 . . . . . . . . . 10 2 ≠ 3
8076, 79pm3.2i 470 . . . . . . . . 9 (2 ≠ 0 ∧ 2 ≠ 3)
8180olci 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}))
8375, 81, 82mp2 9 . . . . . . 7 {0, 2} ≠ {0, 3}
8474, 83pm3.2i 470 . . . . . 6 ({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3})
8515, 43pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
8650orci 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}))
8885, 86, 87mp2 9 . . . . . . 7 {0, 2} ≠ {3, 4}
8915, 55pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0))
9059orci 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}))
9289, 90, 91mp2 9 . . . . . . 7 {0, 2} ≠ {3, 5}
9315, 63pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
9465orci 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}))
9693, 94, 95mp2 9 . . . . . . 7 {0, 2} ≠ {4, 5}
9788, 92, 963pm3.2i 1339 . . . . . 6 ({0, 2} ≠ {3, 4} ∧ {0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5})
9884, 97pm3.2i 470 . . . . 5 (({0, 2} ≠ {1, 2} ∧ {0, 2} ≠ {0, 3}) ∧ ({0, 2} ≠ {3, 4} ∧ {0, 2} ≠ {3, 5} ∧ {0, 2} ≠ {4, 5}))
9923, 32pm3.2i 470 . . . . . . 7 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
10037orci 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}))
10299, 100, 101mp2 9 . . . . . 6 {1, 2} ≠ {0, 3}
10323, 43pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
104 1lt4 12471 . . . . . . . . . . 11 1 < 4
10534, 104ltneii 11405 . . . . . . . . . 10 1 ≠ 4
10636, 105pm3.2i 470 . . . . . . . . 9 (1 ≠ 3 ∧ 1 ≠ 4)
107106orci 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}))
109103, 107, 108mp2 9 . . . . . . 7 {1, 2} ≠ {3, 4}
11023, 55pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0))
111 1lt5 12475 . . . . . . . . . . 11 1 < 5
11234, 111ltneii 11405 . . . . . . . . . 10 1 ≠ 5
11336, 112pm3.2i 470 . . . . . . . . 9 (1 ≠ 3 ∧ 1 ≠ 5)
114113orci 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}))
116110, 114, 115mp2 9 . . . . . . 7 {1, 2} ≠ {3, 5}
11723, 63pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
118105, 112pm3.2i 470 . . . . . . . . 9 (1 ≠ 4 ∧ 1 ≠ 5)
119118orci 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}))
121117, 119, 120mp2 9 . . . . . . 7 {1, 2} ≠ {4, 5}
122109, 116, 1213pm3.2i 1339 . . . . . 6 ({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5})
123102, 122pm3.2i 470 . . . . 5 ({1, 2} ≠ {0, 3} ∧ ({1, 2} ≠ {3, 4} ∧ {1, 2} ≠ {3, 5} ∧ {1, 2} ≠ {4, 5}))
12470, 98, 1233pm3.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})))
12532, 43pm3.2i 470 . . . . . . 7 ((0 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
12650orci 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}))
128125, 126, 127mp2 9 . . . . . 6 {0, 3} ≠ {3, 4}
12932, 55pm3.2i 470 . . . . . . 7 ((0 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0))
13059orci 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}))
132129, 130, 131mp2 9 . . . . . 6 {0, 3} ≠ {3, 5}
13332, 63pm3.2i 470 . . . . . . 7 ((0 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
13465orci 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}))
136133, 134, 135mp2 9 . . . . . 6 {0, 3} ≠ {4, 5}
137128, 132, 1363pm3.2i 1339 . . . . 5 ({0, 3} ≠ {3, 4} ∧ {0, 3} ≠ {3, 5} ∧ {0, 3} ≠ {4, 5})
13843, 55pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0))
139 3re 12375 . . . . . . . . . . 11 3 ∈ ℝ
140 3lt4 12469 . . . . . . . . . . 11 3 < 4
141139, 140ltneii 11405 . . . . . . . . . 10 3 ≠ 4
142141necomi 3001 . . . . . . . . 9 4 ≠ 3
143 4re 12379 . . . . . . . . . 10 4 ∈ ℝ
144 4lt5 12472 . . . . . . . . . 10 4 < 5
145143, 144ltneii 11405 . . . . . . . . 9 4 ≠ 5
146142, 145pm3.2i 470 . . . . . . . 8 (4 ≠ 3 ∧ 4 ≠ 5)
147146olci 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}))
149138, 147, 148mp2 9 . . . . . 6 {3, 4} ≠ {3, 5}
15043, 63pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
151 3lt5 12473 . . . . . . . . . 10 3 < 5
152139, 151ltneii 11405 . . . . . . . . 9 3 ≠ 5
153141, 152pm3.2i 470 . . . . . . . 8 (3 ≠ 4 ∧ 3 ≠ 5)
154153orci 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}))
156150, 154, 155mp2 9 . . . . . 6 {3, 4} ≠ {4, 5}
15755, 63pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
158153orci 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}))
160157, 158, 159mp2 9 . . . . . 6 {3, 5} ≠ {4, 5}
161149, 156, 1603pm3.2i 1339 . . . . 5 ({3, 4} ≠ {3, 5} ∧ {3, 4} ≠ {4, 5} ∧ {3, 5} ≠ {4, 5})
162137, 161pm3.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}))
163124, 162pm3.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})))
16410, 163pm3.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 15017 . . . . . . 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}})))
167166imp 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 14953 . . . . . . . 8 (♯‘⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩) = 7
169168oveq2i 7461 . . . . . . 7 (0..^(♯‘⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩)) = (0..^7)
170 f1oeq2 6853 . . . . . . 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}})))
171169, 170ax-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}}))
172167, 171sylibr 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}}))
173165dmeqi 5929 . . . . . . 7 dom 𝐸 = dom ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩
174 s7cli 14936 . . . . . . . 8 ⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩ ∈ Word V
175 wrddm 14571 . . . . . . . 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}”⟩)))
176174, 175ax-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}”⟩))
177173, 176eqtri 2768 . . . . . 6 dom 𝐸 = (0..^(♯‘⟨“{0, 1} {0, 2} {1, 2} {0, 3} {3, 4} {3, 5} {4, 5}”⟩))
178 f1oeq2 6853 . . . . . 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}})))
179177, 178ax-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}}))
180172, 179sylibr 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 6863 . . . 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}}))
182180, 181syl 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 13683 . . . . . . . . . . 11 (5 ∈ ℕ0 → 0 ∈ (0...5))
18454, 183ax-mp 5 . . . . . . . . . 10 0 ∈ (0...5)
185 5re 12382 . . . . . . . . . . . 12 5 ∈ ℝ
18634, 185, 111ltleii 11415 . . . . . . . . . . 11 1 ≤ 5
187 elfz2nn0 13677 . . . . . . . . . . 11 (1 ∈ (0...5) ↔ (1 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 1 ≤ 5))
18812, 54, 186, 187mpbir3an 1341 . . . . . . . . . 10 1 ∈ (0...5)
189 prssi 4846 . . . . . . . . . 10 ((0 ∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆ (0...5))
190184, 188, 189mp2an 691 . . . . . . . . 9 {0, 1} ⊆ (0...5)
191 2lt5 12474 . . . . . . . . . . . 12 2 < 5
19277, 185, 191ltleii 11415 . . . . . . . . . . 11 2 ≤ 5
193 elfz2nn0 13677 . . . . . . . . . . 11 (2 ∈ (0...5) ↔ (2 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 2 ≤ 5))
19414, 54, 192, 193mpbir3an 1341 . . . . . . . . . 10 2 ∈ (0...5)
195 prssi 4846 . . . . . . . . . 10 ((0 ∈ (0...5) ∧ 2 ∈ (0...5)) → {0, 2} ⊆ (0...5))
196184, 194, 195mp2an 691 . . . . . . . . 9 {0, 2} ⊆ (0...5)
197 prssi 4846 . . . . . . . . . 10 ((1 ∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆ (0...5))
198188, 194, 197mp2an 691 . . . . . . . . 9 {1, 2} ⊆ (0...5)
199 sseq1 4034 . . . . . . . . . . 11 (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
200 sseq1 4034 . . . . . . . . . . 11 (𝑒 = {0, 2} → (𝑒 ⊆ (0...5) ↔ {0, 2} ⊆ (0...5)))
201 sseq1 4034 . . . . . . . . . . 11 (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
202199, 200, 201raltpg 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))))
2034, 202ax-mp 5 . . . . . . . . 9 (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}}𝑒 ⊆ (0...5) ↔ ({0, 1} ⊆ (0...5) ∧ {0, 2} ⊆ (0...5) ∧ {1, 2} ⊆ (0...5)))
204190, 196, 198, 203mpbir3an 1341 . . . . . . . 8 𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}}𝑒 ⊆ (0...5)
205139, 185, 151ltleii 11415 . . . . . . . . . . 11 3 ≤ 5
206 elfz2nn0 13677 . . . . . . . . . . 11 (3 ∈ (0...5) ↔ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 3 ≤ 5))
20731, 54, 205, 206mpbir3an 1341 . . . . . . . . . 10 3 ∈ (0...5)
208 prssi 4846 . . . . . . . . . 10 ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
209184, 207, 208mp2an 691 . . . . . . . . 9 {0, 3} ⊆ (0...5)
210 sseq1 4034 . . . . . . . . . 10 (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
2115, 210ralsn 4705 . . . . . . . . 9 (∀𝑒 ∈ {{0, 3}}𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5))
212209, 211mpbir 231 . . . . . . . 8 𝑒 ∈ {{0, 3}}𝑒 ⊆ (0...5)
213 ralunb 4220 . . . . . . . 8 (∀𝑒 ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}}𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{0, 3}}𝑒 ⊆ (0...5)))
214204, 212, 213mpbir2an 710 . . . . . . 7 𝑒 ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})𝑒 ⊆ (0...5)
215143, 185, 144ltleii 11415 . . . . . . . . . 10 4 ≤ 5
216 elfz2nn0 13677 . . . . . . . . . 10 (4 ∈ (0...5) ↔ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 4 ≤ 5))
21742, 54, 215, 216mpbir3an 1341 . . . . . . . . 9 4 ∈ (0...5)
218 prssi 4846 . . . . . . . . 9 ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
219207, 217, 218mp2an 691 . . . . . . . 8 {3, 4} ⊆ (0...5)
220 nn0fz0 13684 . . . . . . . . . 10 (5 ∈ ℕ0 ↔ 5 ∈ (0...5))
22154, 220mpbi 230 . . . . . . . . 9 5 ∈ (0...5)
222 prssi 4846 . . . . . . . . 9 ((3 ∈ (0...5) ∧ 5 ∈ (0...5)) → {3, 5} ⊆ (0...5))
223207, 221, 222mp2an 691 . . . . . . . 8 {3, 5} ⊆ (0...5)
224 prssi 4846 . . . . . . . . 9 ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
225217, 221, 224mp2an 691 . . . . . . . 8 {4, 5} ⊆ (0...5)
226 sseq1 4034 . . . . . . . . . 10 (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
227 sseq1 4034 . . . . . . . . . 10 (𝑒 = {3, 5} → (𝑒 ⊆ (0...5) ↔ {3, 5} ⊆ (0...5)))
228 sseq1 4034 . . . . . . . . . 10 (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
229226, 227, 228raltpg 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))))
2309, 229ax-mp 5 . . . . . . . 8 (∀𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}}𝑒 ⊆ (0...5) ↔ ({3, 4} ⊆ (0...5) ∧ {3, 5} ⊆ (0...5) ∧ {4, 5} ⊆ (0...5)))
231219, 223, 225, 230mpbir3an 1341 . . . . . . 7 𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}}𝑒 ⊆ (0...5)
232 ralunb 4220 . . . . . . 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)))
233214, 231, 232mpbir2an 710 . . . . . 6 𝑒 ∈ (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})𝑒 ⊆ (0...5)
234 pwssb 5124 . . . . . 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))
235233, 234mpbir 231 . . . . 5 (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆ 𝒫 (0...5)
236 usgrexmpl1.v . . . . . 6 𝑉 = (0...5)
237236pweqi 4638 . . . . 5 𝒫 𝑉 = 𝒫 (0...5)
238235, 237sseqtrri 4046 . . . 4 (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆ 𝒫 𝑉
239 prhash2ex 14450 . . . . . . 7 (♯‘{0, 1}) = 2
240 c0ex 11286 . . . . . . . . 9 0 ∈ V
241 2ex 12372 . . . . . . . . 9 2 ∈ V
242240, 241, 263pm3.2i 1339 . . . . . . . 8 (0 ∈ V ∧ 2 ∈ V ∧ 0 ≠ 2)
243 hashprb 14448 . . . . . . . 8 ((0 ∈ V ∧ 2 ∈ V ∧ 0 ≠ 2) ↔ (♯‘{0, 2}) = 2)
244242, 243mpbi 230 . . . . . . 7 (♯‘{0, 2}) = 2
245 1ex 11288 . . . . . . . . 9 1 ∈ V
246245, 241, 183pm3.2i 1339 . . . . . . . 8 (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
247 hashprb 14448 . . . . . . . 8 ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
248246, 247mpbi 230 . . . . . . 7 (♯‘{1, 2}) = 2
249 fveqeq2 6931 . . . . . . . . 9 (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
250 fveqeq2 6931 . . . . . . . . 9 (𝑒 = {0, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 2}) = 2))
251 fveqeq2 6931 . . . . . . . . 9 (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
252249, 250, 251raltpg 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)))
2534, 252ax-mp 5 . . . . . . 7 (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}} (♯‘𝑒) = 2 ↔ ((♯‘{0, 1}) = 2 ∧ (♯‘{0, 2}) = 2 ∧ (♯‘{1, 2}) = 2))
254239, 244, 248, 253mpbir3an 1341 . . . . . 6 𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}} (♯‘𝑒) = 2
255 3ex 12377 . . . . . . . . 9 3 ∈ V
256240, 255, 473pm3.2i 1339 . . . . . . . 8 (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
257 hashprb 14448 . . . . . . . 8 ((0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3) ↔ (♯‘{0, 3}) = 2)
258256, 257mpbi 230 . . . . . . 7 (♯‘{0, 3}) = 2
259 fveqeq2 6931 . . . . . . . 8 (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
2605, 259ralsn 4705 . . . . . . 7 (∀𝑒 ∈ {{0, 3}} (♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2)
261258, 260mpbir 231 . . . . . 6 𝑒 ∈ {{0, 3}} (♯‘𝑒) = 2
262 ralunb 4220 . . . . . 6 (∀𝑒 ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ {{0, 1}, {0, 2}, {1, 2}} (♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{0, 3}} (♯‘𝑒) = 2))
263254, 261, 262mpbir2an 710 . . . . 5 𝑒 ∈ ({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}})(♯‘𝑒) = 2
264143elexi 3511 . . . . . . . 8 4 ∈ V
265255, 264, 1413pm3.2i 1339 . . . . . . 7 (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
266 hashprb 14448 . . . . . . 7 ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
267265, 266mpbi 230 . . . . . 6 (♯‘{3, 4}) = 2
268185elexi 3511 . . . . . . . 8 5 ∈ V
269255, 268, 1523pm3.2i 1339 . . . . . . 7 (3 ∈ V ∧ 5 ∈ V ∧ 3 ≠ 5)
270 hashprb 14448 . . . . . . 7 ((3 ∈ V ∧ 5 ∈ V ∧ 3 ≠ 5) ↔ (♯‘{3, 5}) = 2)
271269, 270mpbi 230 . . . . . 6 (♯‘{3, 5}) = 2
272264, 268, 1453pm3.2i 1339 . . . . . . 7 (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
273 hashprb 14448 . . . . . . 7 ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
274272, 273mpbi 230 . . . . . 6 (♯‘{4, 5}) = 2
275 fveqeq2 6931 . . . . . . . 8 (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
276 fveqeq2 6931 . . . . . . . 8 (𝑒 = {3, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 5}) = 2))
277 fveqeq2 6931 . . . . . . . 8 (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
278275, 276, 277raltpg 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)))
2799, 278ax-mp 5 . . . . . 6 (∀𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}} (♯‘𝑒) = 2 ↔ ((♯‘{3, 4}) = 2 ∧ (♯‘{3, 5}) = 2 ∧ (♯‘{4, 5}) = 2))
280267, 271, 274, 279mpbir3an 1341 . . . . 5 𝑒 ∈ {{3, 4}, {3, 5}, {4, 5}} (♯‘𝑒) = 2
281 ralunb 4220 . . . . 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))
282263, 280, 281mpbir2an 710 . . . 4 𝑒 ∈ (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}})(♯‘𝑒) = 2
283 ssrab 4096 . . . 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))
284238, 282, 283mpbir2an 710 . . 3 (({{0, 1}, {0, 2}, {1, 2}} ∪ {{0, 3}}) ∪ {{3, 4}, {3, 5}, {4, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
285 f1ss 6824 . . 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})
286182, 284, 285sylancl 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})
287164, 165, 286mp2an 691 1 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wo 846  w3a 1087   = wceq 1537  wcel 2108  wne 2946  wral 3067  {crab 3443  Vcvv 3488  cun 3974  wss 3976  𝒫 cpw 4622  {csn 4648  {cpr 4650  {ctp 4652   class class class wbr 5166  dom cdm 5700  1-1wf1 6572  1-1-ontowf1o 6574  cfv 6575  (class class class)co 7450  cr 11185  0cc0 11186  1c1 11187  cle 11327  2c2 12350  3c3 12351  4c4 12352  5c5 12353  7c7 12355  0cn0 12555  ...cfz 13569  ..^cfzo 13713  chash 14381  Word cword 14564  ⟨“cs7 14897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7772  ax-cnex 11242  ax-resscn 11243  ax-1cn 11244  ax-icn 11245  ax-addcl 11246  ax-addrcl 11247  ax-mulcl 11248  ax-mulrcl 11249  ax-mulcom 11250  ax-addass 11251  ax-mulass 11252  ax-distr 11253  ax-i2m1 11254  ax-1ne0 11255  ax-1rid 11256  ax-rnegex 11257  ax-rrecex 11258  ax-cnre 11259  ax-pre-lttri 11260  ax-pre-lttrn 11261  ax-pre-ltadd 11262  ax-pre-mulgt0 11263
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6334  df-ord 6400  df-on 6401  df-lim 6402  df-suc 6403  df-iota 6527  df-fun 6577  df-fn 6578  df-f 6579  df-f1 6580  df-fo 6581  df-f1o 6582  df-fv 6583  df-riota 7406  df-ov 7453  df-oprab 7454  df-mpo 7455  df-om 7906  df-1st 8032  df-2nd 8033  df-frecs 8324  df-wrecs 8355  df-recs 8429  df-rdg 8468  df-1o 8524  df-2o 8525  df-oadd 8528  df-er 8765  df-en 9006  df-dom 9007  df-sdom 9008  df-fin 9009  df-dju 9972  df-card 10010  df-pnf 11328  df-mnf 11329  df-xr 11330  df-ltxr 11331  df-le 11332  df-sub 11524  df-neg 11525  df-nn 12296  df-2 12358  df-3 12359  df-4 12360  df-5 12361  df-6 12362  df-7 12363  df-n0 12556  df-xnn0 12628  df-z 12642  df-uz 12906  df-fz 13570  df-fzo 13714  df-hash 14382  df-word 14565  df-concat 14621  df-s1 14646  df-s2 14899  df-s3 14900  df-s4 14901  df-s5 14902  df-s6 14903  df-s7 14904
This theorem is referenced by:  usgrexmpl1  47839
  Copyright terms: Public domain W3C validator