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

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

Proof of Theorem usgrexmpl2lem
StepHypRef Expression
1 prex 5452 . . . . 5 {0, 1} ∈ V
2 prex 5452 . . . . 5 {1, 2} ∈ V
3 prex 5452 . . . . 5 {2, 3} ∈ V
41, 2, 33pm3.2i 1339 . . . 4 ({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V)
5 prex 5452 . . . 4 {3, 4} ∈ V
6 prex 5452 . . . . 5 {4, 5} ∈ V
7 prex 5452 . . . . 5 {0, 3} ∈ V
8 prex 5452 . . . . 5 {0, 5} ∈ V
96, 7, 83pm3.2i 1339 . . . 4 ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)
104, 5, 93pm3.2i 1339 . . 3 (({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 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
1512, 14pm3.2i 470 . . . . . . . . 9 (1 ∈ ℕ0 ∧ 2 ∈ ℕ0)
1613, 15pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (1 ∈ ℕ0 ∧ 2 ∈ ℕ0))
17 0ne1 12366 . . . . . . . . . 10 0 ≠ 1
18 0ne2 12502 . . . . . . . . . 10 0 ≠ 2
1917, 18pm3.2i 470 . . . . . . . . 9 (0 ≠ 1 ∧ 0 ≠ 2)
2019orci 864 . . . . . . . 8 ((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2))
21 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (1 ∈ ℕ0 ∧ 2 ∈ ℕ0)) → (((0 ≠ 1 ∧ 0 ≠ 2) ∨ (1 ≠ 1 ∧ 1 ≠ 2)) → {0, 1} ≠ {1, 2}))
2216, 20, 21mp2 9 . . . . . . 7 {0, 1} ≠ {1, 2}
23 3nn0 12573 . . . . . . . . . 10 3 ∈ ℕ0
2414, 23pm3.2i 470 . . . . . . . . 9 (2 ∈ ℕ0 ∧ 3 ∈ ℕ0)
2513, 24pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (2 ∈ ℕ0 ∧ 3 ∈ ℕ0))
26 0re 11294 . . . . . . . . . . 11 0 ∈ ℝ
27 3pos 12400 . . . . . . . . . . 11 0 < 3
2826, 27ltneii 11405 . . . . . . . . . 10 0 ≠ 3
2918, 28pm3.2i 470 . . . . . . . . 9 (0 ≠ 2 ∧ 0 ≠ 3)
3029orci 864 . . . . . . . 8 ((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3))
31 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (2 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((0 ≠ 2 ∧ 0 ≠ 3) ∨ (1 ≠ 2 ∧ 1 ≠ 3)) → {0, 1} ≠ {2, 3}))
3225, 30, 31mp2 9 . . . . . . 7 {0, 1} ≠ {2, 3}
33 4nn0 12574 . . . . . . . . . 10 4 ∈ ℕ0
3423, 33pm3.2i 470 . . . . . . . . 9 (3 ∈ ℕ0 ∧ 4 ∈ ℕ0)
3513, 34pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
36 4pos 12402 . . . . . . . . . . 11 0 < 4
3726, 36ltneii 11405 . . . . . . . . . 10 0 ≠ 4
3828, 37pm3.2i 470 . . . . . . . . 9 (0 ≠ 3 ∧ 0 ≠ 4)
3938orci 864 . . . . . . . 8 ((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4))
40 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0)) → (((0 ≠ 3 ∧ 0 ≠ 4) ∨ (1 ≠ 3 ∧ 1 ≠ 4)) → {0, 1} ≠ {3, 4}))
4135, 39, 40mp2 9 . . . . . . 7 {0, 1} ≠ {3, 4}
4222, 32, 413pm3.2i 1339 . . . . . 6 ({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4})
43 5nn0 12575 . . . . . . . . . 10 5 ∈ ℕ0
4433, 43pm3.2i 470 . . . . . . . . 9 (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)
4513, 44pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
46 5pos 12404 . . . . . . . . . . 11 0 < 5
4726, 46ltneii 11405 . . . . . . . . . 10 0 ≠ 5
4837, 47pm3.2i 470 . . . . . . . . 9 (0 ≠ 4 ∧ 0 ≠ 5)
4948orci 864 . . . . . . . 8 ((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5))
50 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 4 ∧ 0 ≠ 5) ∨ (1 ≠ 4 ∧ 1 ≠ 5)) → {0, 1} ≠ {4, 5}))
5145, 49, 50mp2 9 . . . . . . 7 {0, 1} ≠ {4, 5}
5211, 23pm3.2i 470 . . . . . . . . 9 (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)
5313, 52pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
54 ax-1ne0 11255 . . . . . . . . . 10 1 ≠ 0
55 1re 11292 . . . . . . . . . . 11 1 ∈ ℝ
56 1lt3 12468 . . . . . . . . . . 11 1 < 3
5755, 56ltneii 11405 . . . . . . . . . 10 1 ≠ 3
5854, 57pm3.2i 470 . . . . . . . . 9 (1 ≠ 0 ∧ 1 ≠ 3)
5958olci 865 . . . . . . . 8 ((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3))
60 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((0 ≠ 0 ∧ 0 ≠ 3) ∨ (1 ≠ 0 ∧ 1 ≠ 3)) → {0, 1} ≠ {0, 3}))
6153, 59, 60mp2 9 . . . . . . 7 {0, 1} ≠ {0, 3}
6211, 43pm3.2i 470 . . . . . . . . 9 (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)
6313, 62pm3.2i 470 . . . . . . . 8 ((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
64 1lt5 12475 . . . . . . . . . . 11 1 < 5
6555, 64ltneii 11405 . . . . . . . . . 10 1 ≠ 5
6654, 65pm3.2i 470 . . . . . . . . 9 (1 ≠ 0 ∧ 1 ≠ 5)
6766olci 865 . . . . . . . 8 ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5))
68 prneimg 4879 . . . . . . . 8 (((0 ∈ ℕ0 ∧ 1 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 0 ∧ 0 ≠ 5) ∨ (1 ≠ 0 ∧ 1 ≠ 5)) → {0, 1} ≠ {0, 5}))
6963, 67, 68mp2 9 . . . . . . 7 {0, 1} ≠ {0, 5}
7051, 61, 693pm3.2i 1339 . . . . . 6 ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})
7142, 70pm3.2i 470 . . . . 5 (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5}))
7215, 24pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (2 ∈ ℕ0 ∧ 3 ∈ ℕ0))
73 1ne2 12503 . . . . . . . . . 10 1 ≠ 2
7473, 57pm3.2i 470 . . . . . . . . 9 (1 ≠ 2 ∧ 1 ≠ 3)
7574orci 864 . . . . . . . 8 ((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3))
76 prneimg 4879 . . . . . . . 8 (((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (2 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((1 ≠ 2 ∧ 1 ≠ 3) ∨ (2 ≠ 2 ∧ 2 ≠ 3)) → {1, 2} ≠ {2, 3}))
7772, 75, 76mp2 9 . . . . . . 7 {1, 2} ≠ {2, 3}
7815, 34pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
79 1lt4 12471 . . . . . . . . . . 11 1 < 4
8055, 79ltneii 11405 . . . . . . . . . 10 1 ≠ 4
8157, 80pm3.2i 470 . . . . . . . . 9 (1 ≠ 3 ∧ 1 ≠ 4)
8281orci 864 . . . . . . . 8 ((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4))
83 prneimg 4879 . . . . . . . 8 (((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0)) → (((1 ≠ 3 ∧ 1 ≠ 4) ∨ (2 ≠ 3 ∧ 2 ≠ 4)) → {1, 2} ≠ {3, 4}))
8478, 82, 83mp2 9 . . . . . . 7 {1, 2} ≠ {3, 4}
8577, 84pm3.2i 470 . . . . . 6 ({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4})
8615, 44pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
8780, 65pm3.2i 470 . . . . . . . . 9 (1 ≠ 4 ∧ 1 ≠ 5)
8887orci 864 . . . . . . . 8 ((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5))
89 prneimg 4879 . . . . . . . 8 (((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((1 ≠ 4 ∧ 1 ≠ 5) ∨ (2 ≠ 4 ∧ 2 ≠ 5)) → {1, 2} ≠ {4, 5}))
9086, 88, 89mp2 9 . . . . . . 7 {1, 2} ≠ {4, 5}
9115, 52pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
9258orci 864 . . . . . . . 8 ((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3))
93 prneimg 4879 . . . . . . . 8 (((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((1 ≠ 0 ∧ 1 ≠ 3) ∨ (2 ≠ 0 ∧ 2 ≠ 3)) → {1, 2} ≠ {0, 3}))
9491, 92, 93mp2 9 . . . . . . 7 {1, 2} ≠ {0, 3}
9515, 62pm3.2i 470 . . . . . . . 8 ((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
9666orci 864 . . . . . . . 8 ((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5))
97 prneimg 4879 . . . . . . . 8 (((1 ∈ ℕ0 ∧ 2 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((1 ≠ 0 ∧ 1 ≠ 5) ∨ (2 ≠ 0 ∧ 2 ≠ 5)) → {1, 2} ≠ {0, 5}))
9895, 96, 97mp2 9 . . . . . . 7 {1, 2} ≠ {0, 5}
9990, 94, 983pm3.2i 1339 . . . . . 6 ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})
10085, 99pm3.2i 470 . . . . 5 (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5}))
10124, 34pm3.2i 470 . . . . . . 7 ((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0))
102 2re 12369 . . . . . . . . . 10 2 ∈ ℝ
103 2lt3 12467 . . . . . . . . . 10 2 < 3
104102, 103ltneii 11405 . . . . . . . . 9 2 ≠ 3
105 2lt4 12470 . . . . . . . . . 10 2 < 4
106102, 105ltneii 11405 . . . . . . . . 9 2 ≠ 4
107104, 106pm3.2i 470 . . . . . . . 8 (2 ≠ 3 ∧ 2 ≠ 4)
108107orci 864 . . . . . . 7 ((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4))
109 prneimg 4879 . . . . . . 7 (((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0)) → (((2 ≠ 3 ∧ 2 ≠ 4) ∨ (3 ≠ 3 ∧ 3 ≠ 4)) → {2, 3} ≠ {3, 4}))
110101, 108, 109mp2 9 . . . . . 6 {2, 3} ≠ {3, 4}
11124, 44pm3.2i 470 . . . . . . . 8 ((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
112 2lt5 12474 . . . . . . . . . . 11 2 < 5
113102, 112ltneii 11405 . . . . . . . . . 10 2 ≠ 5
114106, 113pm3.2i 470 . . . . . . . . 9 (2 ≠ 4 ∧ 2 ≠ 5)
115114orci 864 . . . . . . . 8 ((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5))
116 prneimg 4879 . . . . . . . 8 (((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((2 ≠ 4 ∧ 2 ≠ 5) ∨ (3 ≠ 4 ∧ 3 ≠ 5)) → {2, 3} ≠ {4, 5}))
117111, 115, 116mp2 9 . . . . . . 7 {2, 3} ≠ {4, 5}
11824, 52pm3.2i 470 . . . . . . . 8 ((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
119 2ne0 12399 . . . . . . . . . 10 2 ≠ 0
120119, 104pm3.2i 470 . . . . . . . . 9 (2 ≠ 0 ∧ 2 ≠ 3)
121120orci 864 . . . . . . . 8 ((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3))
122 prneimg 4879 . . . . . . . 8 (((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((2 ≠ 0 ∧ 2 ≠ 3) ∨ (3 ≠ 0 ∧ 3 ≠ 3)) → {2, 3} ≠ {0, 3}))
123118, 121, 122mp2 9 . . . . . . 7 {2, 3} ≠ {0, 3}
12424, 62pm3.2i 470 . . . . . . . 8 ((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
125119, 113pm3.2i 470 . . . . . . . . 9 (2 ≠ 0 ∧ 2 ≠ 5)
126125orci 864 . . . . . . . 8 ((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
127 prneimg 4879 . . . . . . . 8 (((2 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((2 ≠ 0 ∧ 2 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5)) → {2, 3} ≠ {0, 5}))
128124, 126, 127mp2 9 . . . . . . 7 {2, 3} ≠ {0, 5}
129117, 123, 1283pm3.2i 1339 . . . . . 6 ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5})
130110, 129pm3.2i 470 . . . . 5 ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))
13171, 100, 1303pm3.2i 1339 . . . 4 ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5})))
13234, 44pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0))
133 3re 12375 . . . . . . . . . 10 3 ∈ ℝ
134 3lt4 12469 . . . . . . . . . 10 3 < 4
135133, 134ltneii 11405 . . . . . . . . 9 3 ≠ 4
136 3lt5 12473 . . . . . . . . . 10 3 < 5
137133, 136ltneii 11405 . . . . . . . . 9 3 ≠ 5
138135, 137pm3.2i 470 . . . . . . . 8 (3 ≠ 4 ∧ 3 ≠ 5)
139138orci 864 . . . . . . 7 ((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5))
140 prneimg 4879 . . . . . . 7 (((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((3 ≠ 4 ∧ 3 ≠ 5) ∨ (4 ≠ 4 ∧ 4 ≠ 5)) → {3, 4} ≠ {4, 5}))
141132, 139, 140mp2 9 . . . . . 6 {3, 4} ≠ {4, 5}
14234, 52pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
143 4ne0 12403 . . . . . . . . 9 4 ≠ 0
144135necomi 3001 . . . . . . . . 9 4 ≠ 3
145143, 144pm3.2i 470 . . . . . . . 8 (4 ≠ 0 ∧ 4 ≠ 3)
146145olci 865 . . . . . . 7 ((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3))
147 prneimg 4879 . . . . . . 7 (((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((3 ≠ 0 ∧ 3 ≠ 3) ∨ (4 ≠ 0 ∧ 4 ≠ 3)) → {3, 4} ≠ {0, 3}))
148142, 146, 147mp2 9 . . . . . 6 {3, 4} ≠ {0, 3}
14934, 62pm3.2i 470 . . . . . . 7 ((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
150 3ne0 12401 . . . . . . . . 9 3 ≠ 0
151150, 137pm3.2i 470 . . . . . . . 8 (3 ≠ 0 ∧ 3 ≠ 5)
152151orci 864 . . . . . . 7 ((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5))
153 prneimg 4879 . . . . . . 7 (((3 ∈ ℕ0 ∧ 4 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((3 ≠ 0 ∧ 3 ≠ 5) ∨ (4 ≠ 0 ∧ 4 ≠ 5)) → {3, 4} ≠ {0, 5}))
154149, 152, 153mp2 9 . . . . . 6 {3, 4} ≠ {0, 5}
155141, 148, 1543pm3.2i 1339 . . . . 5 ({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5})
15644, 52pm3.2i 470 . . . . . . 7 ((4 ∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0))
157145orci 864 . . . . . . 7 ((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3))
158 prneimg 4879 . . . . . . 7 (((4 ∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 3 ∈ ℕ0)) → (((4 ≠ 0 ∧ 4 ≠ 3) ∨ (5 ≠ 0 ∧ 5 ≠ 3)) → {4, 5} ≠ {0, 3}))
159156, 157, 158mp2 9 . . . . . 6 {4, 5} ≠ {0, 3}
16044, 62pm3.2i 470 . . . . . . 7 ((4 ∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
161 4re 12379 . . . . . . . . . 10 4 ∈ ℝ
162 4lt5 12472 . . . . . . . . . 10 4 < 5
163161, 162ltneii 11405 . . . . . . . . 9 4 ≠ 5
164143, 163pm3.2i 470 . . . . . . . 8 (4 ≠ 0 ∧ 4 ≠ 5)
165164orci 864 . . . . . . 7 ((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5))
166 prneimg 4879 . . . . . . 7 (((4 ∈ ℕ0 ∧ 5 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((4 ≠ 0 ∧ 4 ≠ 5) ∨ (5 ≠ 0 ∧ 5 ≠ 5)) → {4, 5} ≠ {0, 5}))
167160, 165, 166mp2 9 . . . . . 6 {4, 5} ≠ {0, 5}
16852, 62pm3.2i 470 . . . . . . 7 ((0 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0))
169151olci 865 . . . . . . 7 ((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5))
170 prneimg 4879 . . . . . . 7 (((0 ∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (0 ∈ ℕ0 ∧ 5 ∈ ℕ0)) → (((0 ≠ 0 ∧ 0 ≠ 5) ∨ (3 ≠ 0 ∧ 3 ≠ 5)) → {0, 3} ≠ {0, 5}))
171168, 169, 170mp2 9 . . . . . 6 {0, 3} ≠ {0, 5}
172159, 167, 1713pm3.2i 1339 . . . . 5 ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})
173155, 172pm3.2i 470 . . . 4 (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5}))
174131, 173pm3.2i 470 . . 3 (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))
17510, 174pm3.2i 470 . 2 ((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5}))))
176 usgrexmpl2.e . 2 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
177 s7f1o 15017 . . . . . . 7 (((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) → (𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ → 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
178177imp 406 . . . . . 6 ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
179 s7len 14953 . . . . . . . 8 (♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) = 7
180179oveq2i 7461 . . . . . . 7 (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7)
181 f1oeq2 6853 . . . . . . 7 ((0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) = (0..^7) → (𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
182180, 181ax-mp 5 . . . . . 6 (𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^7)–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
183178, 182sylibr 234 . . . . 5 ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
184176dmeqi 5929 . . . . . . 7 dom 𝐸 = dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩
185 s7cli 14936 . . . . . . . 8 ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V
186 wrddm 14571 . . . . . . . 8 (⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ ∈ Word V → dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)))
187185, 186ax-mp 5 . . . . . . 7 dom ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩ = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
188184, 187eqtri 2768 . . . . . 6 dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))
189 f1oeq2 6853 . . . . . 6 (dom 𝐸 = (0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩)) → (𝐸:dom 𝐸1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})))
190188, 189ax-mp 5 . . . . 5 (𝐸:dom 𝐸1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ↔ 𝐸:(0..^(♯‘⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩))–1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
191183, 190sylibr 234 . . . 4 ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
192 f1of1 6863 . . . 4 (𝐸:dom 𝐸1-1-onto→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) → 𝐸:dom 𝐸1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
193191, 192syl 17 . . 3 ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}))
194 0elfz 13683 . . . . . . . . . . 11 (5 ∈ ℕ0 → 0 ∈ (0...5))
19543, 194ax-mp 5 . . . . . . . . . 10 0 ∈ (0...5)
196 5re 12382 . . . . . . . . . . . 12 5 ∈ ℝ
19755, 196, 64ltleii 11415 . . . . . . . . . . 11 1 ≤ 5
198 elfz2nn0 13677 . . . . . . . . . . 11 (1 ∈ (0...5) ↔ (1 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 1 ≤ 5))
19912, 43, 197, 198mpbir3an 1341 . . . . . . . . . 10 1 ∈ (0...5)
200 prssi 4846 . . . . . . . . . 10 ((0 ∈ (0...5) ∧ 1 ∈ (0...5)) → {0, 1} ⊆ (0...5))
201195, 199, 200mp2an 691 . . . . . . . . 9 {0, 1} ⊆ (0...5)
202102, 196, 112ltleii 11415 . . . . . . . . . . 11 2 ≤ 5
203 elfz2nn0 13677 . . . . . . . . . . 11 (2 ∈ (0...5) ↔ (2 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 2 ≤ 5))
20414, 43, 202, 203mpbir3an 1341 . . . . . . . . . 10 2 ∈ (0...5)
205 prssi 4846 . . . . . . . . . 10 ((1 ∈ (0...5) ∧ 2 ∈ (0...5)) → {1, 2} ⊆ (0...5))
206199, 204, 205mp2an 691 . . . . . . . . 9 {1, 2} ⊆ (0...5)
207133, 196, 136ltleii 11415 . . . . . . . . . . 11 3 ≤ 5
208 elfz2nn0 13677 . . . . . . . . . . 11 (3 ∈ (0...5) ↔ (3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 3 ≤ 5))
20923, 43, 207, 208mpbir3an 1341 . . . . . . . . . 10 3 ∈ (0...5)
210 prssi 4846 . . . . . . . . . 10 ((2 ∈ (0...5) ∧ 3 ∈ (0...5)) → {2, 3} ⊆ (0...5))
211204, 209, 210mp2an 691 . . . . . . . . 9 {2, 3} ⊆ (0...5)
212 sseq1 4034 . . . . . . . . . 10 (𝑒 = {0, 1} → (𝑒 ⊆ (0...5) ↔ {0, 1} ⊆ (0...5)))
213 sseq1 4034 . . . . . . . . . 10 (𝑒 = {1, 2} → (𝑒 ⊆ (0...5) ↔ {1, 2} ⊆ (0...5)))
214 sseq1 4034 . . . . . . . . . 10 (𝑒 = {2, 3} → (𝑒 ⊆ (0...5) ↔ {2, 3} ⊆ (0...5)))
2151, 2, 3, 212, 213, 214raltp 4730 . . . . . . . . 9 (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5) ↔ ({0, 1} ⊆ (0...5) ∧ {1, 2} ⊆ (0...5) ∧ {2, 3} ⊆ (0...5)))
216201, 206, 211, 215mpbir3an 1341 . . . . . . . 8 𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5)
217161, 196, 162ltleii 11415 . . . . . . . . . . 11 4 ≤ 5
218 elfz2nn0 13677 . . . . . . . . . . 11 (4 ∈ (0...5) ↔ (4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 4 ≤ 5))
21933, 43, 217, 218mpbir3an 1341 . . . . . . . . . 10 4 ∈ (0...5)
220 prssi 4846 . . . . . . . . . 10 ((3 ∈ (0...5) ∧ 4 ∈ (0...5)) → {3, 4} ⊆ (0...5))
221209, 219, 220mp2an 691 . . . . . . . . 9 {3, 4} ⊆ (0...5)
222 sseq1 4034 . . . . . . . . . 10 (𝑒 = {3, 4} → (𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5)))
2235, 222ralsn 4705 . . . . . . . . 9 (∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5) ↔ {3, 4} ⊆ (0...5))
224221, 223mpbir 231 . . . . . . . 8 𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)
225 ralunb 4220 . . . . . . . 8 (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}}𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{3, 4}}𝑒 ⊆ (0...5)))
226216, 224, 225mpbir2an 710 . . . . . . 7 𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5)
227196leidi 11826 . . . . . . . . . 10 5 ≤ 5
228 elfz2nn0 13677 . . . . . . . . . 10 (5 ∈ (0...5) ↔ (5 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 5 ≤ 5))
22943, 43, 227, 228mpbir3an 1341 . . . . . . . . 9 5 ∈ (0...5)
230 prssi 4846 . . . . . . . . 9 ((4 ∈ (0...5) ∧ 5 ∈ (0...5)) → {4, 5} ⊆ (0...5))
231219, 229, 230mp2an 691 . . . . . . . 8 {4, 5} ⊆ (0...5)
232 prssi 4846 . . . . . . . . 9 ((0 ∈ (0...5) ∧ 3 ∈ (0...5)) → {0, 3} ⊆ (0...5))
233195, 209, 232mp2an 691 . . . . . . . 8 {0, 3} ⊆ (0...5)
234 prssi 4846 . . . . . . . . 9 ((0 ∈ (0...5) ∧ 5 ∈ (0...5)) → {0, 5} ⊆ (0...5))
235195, 229, 234mp2an 691 . . . . . . . 8 {0, 5} ⊆ (0...5)
236 sseq1 4034 . . . . . . . . 9 (𝑒 = {4, 5} → (𝑒 ⊆ (0...5) ↔ {4, 5} ⊆ (0...5)))
237 sseq1 4034 . . . . . . . . 9 (𝑒 = {0, 3} → (𝑒 ⊆ (0...5) ↔ {0, 3} ⊆ (0...5)))
238 sseq1 4034 . . . . . . . . 9 (𝑒 = {0, 5} → (𝑒 ⊆ (0...5) ↔ {0, 5} ⊆ (0...5)))
2396, 7, 8, 236, 237, 238raltp 4730 . . . . . . . 8 (∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5) ↔ ({4, 5} ⊆ (0...5) ∧ {0, 3} ⊆ (0...5) ∧ {0, 5} ⊆ (0...5)))
240231, 233, 235, 239mpbir3an 1341 . . . . . . 7 𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5)
241 ralunb 4220 . . . . . . 7 (∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5) ↔ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})𝑒 ⊆ (0...5) ∧ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}}𝑒 ⊆ (0...5)))
242226, 240, 241mpbir2an 710 . . . . . 6 𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5)
243 pwssb 5124 . . . . . 6 ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 (0...5) ↔ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})𝑒 ⊆ (0...5))
244242, 243mpbir 231 . . . . 5 (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 (0...5)
245 usgrexmpl2.v . . . . . 6 𝑉 = (0...5)
246245pweqi 4638 . . . . 5 𝒫 𝑉 = 𝒫 (0...5)
247244, 246sseqtrri 4046 . . . 4 (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉
248 prhash2ex 14450 . . . . . . 7 (♯‘{0, 1}) = 2
249 1ex 11288 . . . . . . . . 9 1 ∈ V
250 2ex 12372 . . . . . . . . 9 2 ∈ V
251249, 250, 733pm3.2i 1339 . . . . . . . 8 (1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2)
252 hashprb 14448 . . . . . . . 8 ((1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2) ↔ (♯‘{1, 2}) = 2)
253251, 252mpbi 230 . . . . . . 7 (♯‘{1, 2}) = 2
254 3ex 12377 . . . . . . . . 9 3 ∈ V
255250, 254, 1043pm3.2i 1339 . . . . . . . 8 (2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3)
256 hashprb 14448 . . . . . . . 8 ((2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3) ↔ (♯‘{2, 3}) = 2)
257255, 256mpbi 230 . . . . . . 7 (♯‘{2, 3}) = 2
258 fveqeq2 6931 . . . . . . . 8 (𝑒 = {0, 1} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 1}) = 2))
259 fveqeq2 6931 . . . . . . . 8 (𝑒 = {1, 2} → ((♯‘𝑒) = 2 ↔ (♯‘{1, 2}) = 2))
260 fveqeq2 6931 . . . . . . . 8 (𝑒 = {2, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{2, 3}) = 2))
2611, 2, 3, 258, 259, 260raltp 4730 . . . . . . 7 (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2 ↔ ((♯‘{0, 1}) = 2 ∧ (♯‘{1, 2}) = 2 ∧ (♯‘{2, 3}) = 2))
262248, 253, 257, 261mpbir3an 1341 . . . . . 6 𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2
26333elexi 3511 . . . . . . . . 9 4 ∈ V
264254, 263, 1353pm3.2i 1339 . . . . . . . 8 (3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4)
265 hashprb 14448 . . . . . . . 8 ((3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4) ↔ (♯‘{3, 4}) = 2)
266264, 265mpbi 230 . . . . . . 7 (♯‘{3, 4}) = 2
267 fveqeq2 6931 . . . . . . . 8 (𝑒 = {3, 4} → ((♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2))
2685, 267ralsn 4705 . . . . . . 7 (∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2 ↔ (♯‘{3, 4}) = 2)
269266, 268mpbir 231 . . . . . 6 𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2
270 ralunb 4220 . . . . . 6 (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ {{0, 1}, {1, 2}, {2, 3}} (♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{3, 4}} (♯‘𝑒) = 2))
271262, 269, 270mpbir2an 710 . . . . 5 𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2
27243elexi 3511 . . . . . . . 8 5 ∈ V
273263, 272, 1633pm3.2i 1339 . . . . . . 7 (4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5)
274 hashprb 14448 . . . . . . 7 ((4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5) ↔ (♯‘{4, 5}) = 2)
275273, 274mpbi 230 . . . . . 6 (♯‘{4, 5}) = 2
276 c0ex 11286 . . . . . . . 8 0 ∈ V
277276, 254, 283pm3.2i 1339 . . . . . . 7 (0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3)
278 hashprb 14448 . . . . . . 7 ((0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3) ↔ (♯‘{0, 3}) = 2)
279277, 278mpbi 230 . . . . . 6 (♯‘{0, 3}) = 2
280276, 272, 473pm3.2i 1339 . . . . . . 7 (0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5)
281 hashprb 14448 . . . . . . 7 ((0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5) ↔ (♯‘{0, 5}) = 2)
282280, 281mpbi 230 . . . . . 6 (♯‘{0, 5}) = 2
283 fveqeq2 6931 . . . . . . 7 (𝑒 = {4, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{4, 5}) = 2))
284 fveqeq2 6931 . . . . . . 7 (𝑒 = {0, 3} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 3}) = 2))
285 fveqeq2 6931 . . . . . . 7 (𝑒 = {0, 5} → ((♯‘𝑒) = 2 ↔ (♯‘{0, 5}) = 2))
2866, 7, 8, 283, 284, 285raltp 4730 . . . . . 6 (∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2 ↔ ((♯‘{4, 5}) = 2 ∧ (♯‘{0, 3}) = 2 ∧ (♯‘{0, 5}) = 2))
287275, 279, 282, 286mpbir3an 1341 . . . . 5 𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2
288 ralunb 4220 . . . . 5 (∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2 ↔ (∀𝑒 ∈ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}})(♯‘𝑒) = 2 ∧ ∀𝑒 ∈ {{4, 5}, {0, 3}, {0, 5}} (♯‘𝑒) = 2))
289271, 287, 288mpbir2an 710 . . . 4 𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2
290 ssrab 4096 . . . 4 ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ ((({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ 𝒫 𝑉 ∧ ∀𝑒 ∈ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}})(♯‘𝑒) = 2))
291247, 289, 290mpbir2an 710 . . 3 (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
292 f1ss 6824 . . 3 ((𝐸:dom 𝐸1-1→(({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ∧ (({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}}) ∪ {{4, 5}, {0, 3}, {0, 5}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}) → 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
293193, 291, 292sylancl 585 . 2 ((((({0, 1} ∈ V ∧ {1, 2} ∈ V ∧ {2, 3} ∈ V) ∧ {3, 4} ∈ V ∧ ({4, 5} ∈ V ∧ {0, 3} ∈ V ∧ {0, 5} ∈ V)) ∧ (((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 3} ∧ {0, 1} ≠ {3, 4}) ∧ ({0, 1} ≠ {4, 5} ∧ {0, 1} ≠ {0, 3} ∧ {0, 1} ≠ {0, 5})) ∧ (({1, 2} ≠ {2, 3} ∧ {1, 2} ≠ {3, 4}) ∧ ({1, 2} ≠ {4, 5} ∧ {1, 2} ≠ {0, 3} ∧ {1, 2} ≠ {0, 5})) ∧ ({2, 3} ≠ {3, 4} ∧ ({2, 3} ≠ {4, 5} ∧ {2, 3} ≠ {0, 3} ∧ {2, 3} ≠ {0, 5}))) ∧ (({3, 4} ≠ {4, 5} ∧ {3, 4} ≠ {0, 3} ∧ {3, 4} ≠ {0, 5}) ∧ ({4, 5} ≠ {0, 3} ∧ {4, 5} ≠ {0, 5} ∧ {0, 3} ≠ {0, 5})))) ∧ 𝐸 = ⟨“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”⟩) → 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
294175, 176, 293mp2an 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  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:  usgrexmpl2  47844
  Copyright terms: Public domain W3C validator