Metamath Proof Explorer

Theorem usgrexmpl2lem

Description: Lemma for usgrexmpl2 . (Contributed by AV, 3-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
Assertion usgrexmpl2lem 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 prex ⊢ { 0 , 1 } ∈ V
4 prex ⊢ { 1 , 2 } ∈ V
5 prex ⊢ { 2 , 3 } ∈ V
6 3 4 5 3pm3.2i ⊢ ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ∧ { 2 , 3 } ∈ V )
7 prex ⊢ { 3 , 4 } ∈ V
8 prex ⊢ { 4 , 5 } ∈ V
9 prex ⊢ { 0 , 3 } ∈ V
10 prex ⊢ { 0 , 5 } ∈ V
11 8 9 10 3pm3.2i ⊢ ( { 4 , 5 } ∈ V ∧ { 0 , 3 } ∈ V ∧ { 0 , 5 } ∈ V )
12 6 7 11 3pm3.2i ⊢ ( ( { 0 , 1 } ∈ V ∧ { 1 , 2 } ∈ V ∧ { 2 , 3 } ∈ V ) ∧ { 3 , 4 } ∈ V ∧ ( { 4 , 5 } ∈ V ∧ { 0 , 3 } ∈ V ∧ { 0 , 5 } ∈ V ) )
13 0nn0 ⊢ 0 ∈ ℕ0
14 1nn0 ⊢ 1 ∈ ℕ0
15 13 14 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 )
16 2nn0 ⊢ 2 ∈ ℕ0
17 14 16 pm3.2i ⊢ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 )
18 15 17 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) )
19 0ne1 ⊢ 0 ≠ 1
20 0ne2 ⊢ 0 ≠ 2
21 19 20 pm3.2i ⊢ ( 0 ≠ 1 ∧ 0 ≠ 2 )
22 21 orci ⊢ ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) )
23 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 1 ∧ 0 ≠ 2 ) ∨ ( 1 ≠ 1 ∧ 1 ≠ 2 ) ) → { 0 , 1 } ≠ { 1 , 2 } ) )
24 18 22 23 mp2 ⊢ { 0 , 1 } ≠ { 1 , 2 }
25 3nn0 ⊢ 3 ∈ ℕ0
26 16 25 pm3.2i ⊢ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 )
27 15 26 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
28 0re ⊢ 0 ∈ ℝ
29 3pos ⊢ 0 < 3
30 28 29 ltneii ⊢ 0 ≠ 3
31 20 30 pm3.2i ⊢ ( 0 ≠ 2 ∧ 0 ≠ 3 )
32 31 orci ⊢ ( ( 0 ≠ 2 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 2 ∧ 1 ≠ 3 ) )
33 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 2 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 2 ∧ 1 ≠ 3 ) ) → { 0 , 1 } ≠ { 2 , 3 } ) )
34 27 32 33 mp2 ⊢ { 0 , 1 } ≠ { 2 , 3 }
35 4nn0 ⊢ 4 ∈ ℕ0
36 25 35 pm3.2i ⊢ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 )
37 15 36 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
38 4pos ⊢ 0 < 4
39 28 38 ltneii ⊢ 0 ≠ 4
40 30 39 pm3.2i ⊢ ( 0 ≠ 3 ∧ 0 ≠ 4 )
41 40 orci ⊢ ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 4 ) )
42 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 3 ∧ 0 ≠ 4 ) ∨ ( 1 ≠ 3 ∧ 1 ≠ 4 ) ) → { 0 , 1 } ≠ { 3 , 4 } ) )
43 37 41 42 mp2 ⊢ { 0 , 1 } ≠ { 3 , 4 }
44 24 34 43 3pm3.2i ⊢ ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 3 } ∧ { 0 , 1 } ≠ { 3 , 4 } )
45 5nn0 ⊢ 5 ∈ ℕ0
46 35 45 pm3.2i ⊢ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
47 15 46 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
48 5pos ⊢ 0 < 5
49 28 48 ltneii ⊢ 0 ≠ 5
50 39 49 pm3.2i ⊢ ( 0 ≠ 4 ∧ 0 ≠ 5 )
51 50 orci ⊢ ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 4 ∧ 1 ≠ 5 ) )
52 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 4 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 4 ∧ 1 ≠ 5 ) ) → { 0 , 1 } ≠ { 4 , 5 } ) )
53 47 51 52 mp2 ⊢ { 0 , 1 } ≠ { 4 , 5 }
54 13 25 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 )
55 15 54 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
56 ax-1ne0 ⊢ 1 ≠ 0
57 1re ⊢ 1 ∈ ℝ
58 1lt3 ⊢ 1 < 3
59 57 58 ltneii ⊢ 1 ≠ 3
60 56 59 pm3.2i ⊢ ( 1 ≠ 0 ∧ 1 ≠ 3 )
61 60 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) )
62 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 3 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 3 ) ) → { 0 , 1 } ≠ { 0 , 3 } ) )
63 55 61 62 mp2 ⊢ { 0 , 1 } ≠ { 0 , 3 }
64 13 45 pm3.2i ⊢ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 )
65 15 64 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
66 1lt5 ⊢ 1 < 5
67 57 66 ltneii ⊢ 1 ≠ 5
68 56 67 pm3.2i ⊢ ( 1 ≠ 0 ∧ 1 ≠ 5 )
69 68 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 5 ) )
70 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 1 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 5 ) ∨ ( 1 ≠ 0 ∧ 1 ≠ 5 ) ) → { 0 , 1 } ≠ { 0 , 5 } ) )
71 65 69 70 mp2 ⊢ { 0 , 1 } ≠ { 0 , 5 }
72 53 63 71 3pm3.2i ⊢ ( { 0 , 1 } ≠ { 4 , 5 } ∧ { 0 , 1 } ≠ { 0 , 3 } ∧ { 0 , 1 } ≠ { 0 , 5 } )
73 44 72 pm3.2i ⊢ ( ( { 0 , 1 } ≠ { 1 , 2 } ∧ { 0 , 1 } ≠ { 2 , 3 } ∧ { 0 , 1 } ≠ { 3 , 4 } ) ∧ ( { 0 , 1 } ≠ { 4 , 5 } ∧ { 0 , 1 } ≠ { 0 , 3 } ∧ { 0 , 1 } ≠ { 0 , 5 } ) )
74 17 26 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
75 1ne2 ⊢ 1 ≠ 2
76 75 59 pm3.2i ⊢ ( 1 ≠ 2 ∧ 1 ≠ 3 )
77 76 orci ⊢ ( ( 1 ≠ 2 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 2 ∧ 2 ≠ 3 ) )
78 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 2 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 2 ∧ 2 ≠ 3 ) ) → { 1 , 2 } ≠ { 2 , 3 } ) )
79 74 77 78 mp2 ⊢ { 1 , 2 } ≠ { 2 , 3 }
80 17 36 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
81 1lt4 ⊢ 1 < 4
82 57 81 ltneii ⊢ 1 ≠ 4
83 59 82 pm3.2i ⊢ ( 1 ≠ 3 ∧ 1 ≠ 4 )
84 83 orci ⊢ ( ( 1 ≠ 3 ∧ 1 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) )
85 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 3 ∧ 1 ≠ 4 ) ∨ ( 2 ≠ 3 ∧ 2 ≠ 4 ) ) → { 1 , 2 } ≠ { 3 , 4 } ) )
86 80 84 85 mp2 ⊢ { 1 , 2 } ≠ { 3 , 4 }
87 79 86 pm3.2i ⊢ ( { 1 , 2 } ≠ { 2 , 3 } ∧ { 1 , 2 } ≠ { 3 , 4 } )
88 17 46 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
89 82 67 pm3.2i ⊢ ( 1 ≠ 4 ∧ 1 ≠ 5 )
90 89 orci ⊢ ( ( 1 ≠ 4 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) )
91 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 4 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 4 ∧ 2 ≠ 5 ) ) → { 1 , 2 } ≠ { 4 , 5 } ) )
92 88 90 91 mp2 ⊢ { 1 , 2 } ≠ { 4 , 5 }
93 17 54 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
94 60 orci ⊢ ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) )
95 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 0 ∧ 1 ≠ 3 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 3 ) ) → { 1 , 2 } ≠ { 0 , 3 } ) )
96 93 94 95 mp2 ⊢ { 1 , 2 } ≠ { 0 , 3 }
97 17 64 pm3.2i ⊢ ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
98 68 orci ⊢ ( ( 1 ≠ 0 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 5 ) )
99 prneimg ⊢ ( ( ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 1 ≠ 0 ∧ 1 ≠ 5 ) ∨ ( 2 ≠ 0 ∧ 2 ≠ 5 ) ) → { 1 , 2 } ≠ { 0 , 5 } ) )
100 97 98 99 mp2 ⊢ { 1 , 2 } ≠ { 0 , 5 }
101 92 96 100 3pm3.2i ⊢ ( { 1 , 2 } ≠ { 4 , 5 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 1 , 2 } ≠ { 0 , 5 } )
102 87 101 pm3.2i ⊢ ( ( { 1 , 2 } ≠ { 2 , 3 } ∧ { 1 , 2 } ≠ { 3 , 4 } ) ∧ ( { 1 , 2 } ≠ { 4 , 5 } ∧ { 1 , 2 } ≠ { 0 , 3 } ∧ { 1 , 2 } ≠ { 0 , 5 } ) )
103 26 36 pm3.2i ⊢ ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) )
104 2re ⊢ 2 ∈ ℝ
105 2lt3 ⊢ 2 < 3
106 104 105 ltneii ⊢ 2 ≠ 3
107 2lt4 ⊢ 2 < 4
108 104 107 ltneii ⊢ 2 ≠ 4
109 106 108 pm3.2i ⊢ ( 2 ≠ 3 ∧ 2 ≠ 4 )
110 109 orci ⊢ ( ( 2 ≠ 3 ∧ 2 ≠ 4 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 4 ) )
111 prneimg ⊢ ( ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 3 ∧ 2 ≠ 4 ) ∨ ( 3 ≠ 3 ∧ 3 ≠ 4 ) ) → { 2 , 3 } ≠ { 3 , 4 } ) )
112 103 110 111 mp2 ⊢ { 2 , 3 } ≠ { 3 , 4 }
113 26 46 pm3.2i ⊢ ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
114 2lt5 ⊢ 2 < 5
115 104 114 ltneii ⊢ 2 ≠ 5
116 108 115 pm3.2i ⊢ ( 2 ≠ 4 ∧ 2 ≠ 5 )
117 116 orci ⊢ ( ( 2 ≠ 4 ∧ 2 ≠ 5 ) ∨ ( 3 ≠ 4 ∧ 3 ≠ 5 ) )
118 prneimg ⊢ ( ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 4 ∧ 2 ≠ 5 ) ∨ ( 3 ≠ 4 ∧ 3 ≠ 5 ) ) → { 2 , 3 } ≠ { 4 , 5 } ) )
119 113 117 118 mp2 ⊢ { 2 , 3 } ≠ { 4 , 5 }
120 26 54 pm3.2i ⊢ ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
121 2ne0 ⊢ 2 ≠ 0
122 121 106 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 3 )
123 122 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 3 ) )
124 prneimg ⊢ ( ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 3 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 3 ) ) → { 2 , 3 } ≠ { 0 , 3 } ) )
125 120 123 124 mp2 ⊢ { 2 , 3 } ≠ { 0 , 3 }
126 26 64 pm3.2i ⊢ ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
127 121 115 pm3.2i ⊢ ( 2 ≠ 0 ∧ 2 ≠ 5 )
128 127 orci ⊢ ( ( 2 ≠ 0 ∧ 2 ≠ 5 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 5 ) )
129 prneimg ⊢ ( ( ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 2 ≠ 0 ∧ 2 ≠ 5 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 5 ) ) → { 2 , 3 } ≠ { 0 , 5 } ) )
130 126 128 129 mp2 ⊢ { 2 , 3 } ≠ { 0 , 5 }
131 119 125 130 3pm3.2i ⊢ ( { 2 , 3 } ≠ { 4 , 5 } ∧ { 2 , 3 } ≠ { 0 , 3 } ∧ { 2 , 3 } ≠ { 0 , 5 } )
132 112 131 pm3.2i ⊢ ( { 2 , 3 } ≠ { 3 , 4 } ∧ ( { 2 , 3 } ≠ { 4 , 5 } ∧ { 2 , 3 } ≠ { 0 , 3 } ∧ { 2 , 3 } ≠ { 0 , 5 } ) )
133 73 102 132 3pm3.2i ⊢ ( ( ( { 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 } ) ) )
134 36 46 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
135 3re ⊢ 3 ∈ ℝ
136 3lt4 ⊢ 3 < 4
137 135 136 ltneii ⊢ 3 ≠ 4
138 3lt5 ⊢ 3 < 5
139 135 138 ltneii ⊢ 3 ≠ 5
140 137 139 pm3.2i ⊢ ( 3 ≠ 4 ∧ 3 ≠ 5 )
141 140 orci ⊢ ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 4 ∧ 4 ≠ 5 ) )
142 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 4 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 4 ∧ 4 ≠ 5 ) ) → { 3 , 4 } ≠ { 4 , 5 } ) )
143 134 141 142 mp2 ⊢ { 3 , 4 } ≠ { 4 , 5 }
144 36 54 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
145 4ne0 ⊢ 4 ≠ 0
146 137 necomi ⊢ 4 ≠ 3
147 145 146 pm3.2i ⊢ ( 4 ≠ 0 ∧ 4 ≠ 3 )
148 147 olci ⊢ ( ( 3 ≠ 0 ∧ 3 ≠ 3 ) ∨ ( 4 ≠ 0 ∧ 4 ≠ 3 ) )
149 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 0 ∧ 3 ≠ 3 ) ∨ ( 4 ≠ 0 ∧ 4 ≠ 3 ) ) → { 3 , 4 } ≠ { 0 , 3 } ) )
150 144 148 149 mp2 ⊢ { 3 , 4 } ≠ { 0 , 3 }
151 36 64 pm3.2i ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
152 3ne0 ⊢ 3 ≠ 0
153 152 139 pm3.2i ⊢ ( 3 ≠ 0 ∧ 3 ≠ 5 )
154 153 orci ⊢ ( ( 3 ≠ 0 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 0 ∧ 4 ≠ 5 ) )
155 prneimg ⊢ ( ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 3 ≠ 0 ∧ 3 ≠ 5 ) ∨ ( 4 ≠ 0 ∧ 4 ≠ 5 ) ) → { 3 , 4 } ≠ { 0 , 5 } ) )
156 151 154 155 mp2 ⊢ { 3 , 4 } ≠ { 0 , 5 }
157 143 150 156 3pm3.2i ⊢ ( { 3 , 4 } ≠ { 4 , 5 } ∧ { 3 , 4 } ≠ { 0 , 3 } ∧ { 3 , 4 } ≠ { 0 , 5 } )
158 46 54 pm3.2i ⊢ ( ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) )
159 147 orci ⊢ ( ( 4 ≠ 0 ∧ 4 ≠ 3 ) ∨ ( 5 ≠ 0 ∧ 5 ≠ 3 ) )
160 prneimg ⊢ ( ( ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ) → ( ( ( 4 ≠ 0 ∧ 4 ≠ 3 ) ∨ ( 5 ≠ 0 ∧ 5 ≠ 3 ) ) → { 4 , 5 } ≠ { 0 , 3 } ) )
161 158 159 160 mp2 ⊢ { 4 , 5 } ≠ { 0 , 3 }
162 46 64 pm3.2i ⊢ ( ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
163 4re ⊢ 4 ∈ ℝ
164 4lt5 ⊢ 4 < 5
165 163 164 ltneii ⊢ 4 ≠ 5
166 145 165 pm3.2i ⊢ ( 4 ≠ 0 ∧ 4 ≠ 5 )
167 166 orci ⊢ ( ( 4 ≠ 0 ∧ 4 ≠ 5 ) ∨ ( 5 ≠ 0 ∧ 5 ≠ 5 ) )
168 prneimg ⊢ ( ( ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 4 ≠ 0 ∧ 4 ≠ 5 ) ∨ ( 5 ≠ 0 ∧ 5 ≠ 5 ) ) → { 4 , 5 } ≠ { 0 , 5 } ) )
169 162 167 168 mp2 ⊢ { 4 , 5 } ≠ { 0 , 5 }
170 54 64 pm3.2i ⊢ ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) )
171 153 olci ⊢ ( ( 0 ≠ 0 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 5 ) )
172 prneimg ⊢ ( ( ( 0 ∈ ℕ0 ∧ 3 ∈ ℕ0 ) ∧ ( 0 ∈ ℕ0 ∧ 5 ∈ ℕ0 ) ) → ( ( ( 0 ≠ 0 ∧ 0 ≠ 5 ) ∨ ( 3 ≠ 0 ∧ 3 ≠ 5 ) ) → { 0 , 3 } ≠ { 0 , 5 } ) )
173 170 171 172 mp2 ⊢ { 0 , 3 } ≠ { 0 , 5 }
174 161 169 173 3pm3.2i ⊢ ( { 4 , 5 } ≠ { 0 , 3 } ∧ { 4 , 5 } ≠ { 0 , 5 } ∧ { 0 , 3 } ≠ { 0 , 5 } )
175 157 174 pm3.2i ⊢ ( ( { 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 133 175 pm3.2i ⊢ ( ( ( ( { 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 } ) ) )
177 12 176 pm3.2i ⊢ ( ( ( { 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 } ) ) ) )
178 s7f1o ⊢ ( ( ( ( { 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 178 imp ⊢ ( ( ( ( ( { 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 } } ) )
180 s7len ⊢ ( ♯ ‘ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ) = 7
181 180 oveq2i ⊢ ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ) ) = ( 0 ..^ 7 )
182 f1oeq2 ⊢ ( ( 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 } } ) ) )
183 181 182 ax-mp ⊢ ( 𝐸 : ( 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 } } ) )
184 179 183 sylibr ⊢ ( ( ( ( ( { 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 } } ) )
185 2 dmeqi ⊢ dom 𝐸 = dom ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
186 s7cli ⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ∈ Word V
187 wrddm ⊢ ( ⟨“ { 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 } ”⟩ ) ) )
188 186 187 ax-mp ⊢ 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 } ”⟩ ) )
189 185 188 eqtri ⊢ dom 𝐸 = ( 0 ..^ ( ♯ ‘ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ) )
190 f1oeq2 ⊢ ( 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 } } ) ) )
191 189 190 ax-mp ⊢ ( 𝐸 : 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 } } ) )
192 184 191 sylibr ⊢ ( ( ( ( ( { 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 } } ) )
193 f1of1 ⊢ ( 𝐸 : 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 } } ) )
194 192 193 syl ⊢ ( ( ( ( ( { 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 } } ) )
195 0elfz ⊢ ( 5 ∈ ℕ0 → 0 ∈ ( 0 ... 5 ) )
196 45 195 ax-mp ⊢ 0 ∈ ( 0 ... 5 )
197 5re ⊢ 5 ∈ ℝ
198 57 197 66 ltleii ⊢ 1 ≤ 5
199 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 5 ) ↔ ( 1 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 1 ≤ 5 ) )
200 14 45 198 199 mpbir3an ⊢ 1 ∈ ( 0 ... 5 )
201 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 1 ∈ ( 0 ... 5 ) ) → { 0 , 1 } ⊆ ( 0 ... 5 ) )
202 196 200 201 mp2an ⊢ { 0 , 1 } ⊆ ( 0 ... 5 )
203 104 197 114 ltleii ⊢ 2 ≤ 5
204 elfz2nn0 ⊢ ( 2 ∈ ( 0 ... 5 ) ↔ ( 2 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 2 ≤ 5 ) )
205 16 45 203 204 mpbir3an ⊢ 2 ∈ ( 0 ... 5 )
206 prssi ⊢ ( ( 1 ∈ ( 0 ... 5 ) ∧ 2 ∈ ( 0 ... 5 ) ) → { 1 , 2 } ⊆ ( 0 ... 5 ) )
207 200 205 206 mp2an ⊢ { 1 , 2 } ⊆ ( 0 ... 5 )
208 135 197 138 ltleii ⊢ 3 ≤ 5
209 elfz2nn0 ⊢ ( 3 ∈ ( 0 ... 5 ) ↔ ( 3 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 3 ≤ 5 ) )
210 25 45 208 209 mpbir3an ⊢ 3 ∈ ( 0 ... 5 )
211 prssi ⊢ ( ( 2 ∈ ( 0 ... 5 ) ∧ 3 ∈ ( 0 ... 5 ) ) → { 2 , 3 } ⊆ ( 0 ... 5 ) )
212 205 210 211 mp2an ⊢ { 2 , 3 } ⊆ ( 0 ... 5 )
213 sseq1 ⊢ ( 𝑒 = { 0 , 1 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 1 } ⊆ ( 0 ... 5 ) ) )
214 sseq1 ⊢ ( 𝑒 = { 1 , 2 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 1 , 2 } ⊆ ( 0 ... 5 ) ) )
215 sseq1 ⊢ ( 𝑒 = { 2 , 3 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 2 , 3 } ⊆ ( 0 ... 5 ) ) )
216 3 4 5 213 214 215 raltp ⊢ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 0 , 1 } ⊆ ( 0 ... 5 ) ∧ { 1 , 2 } ⊆ ( 0 ... 5 ) ∧ { 2 , 3 } ⊆ ( 0 ... 5 ) ) )
217 202 207 212 216 mpbir3an ⊢ ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } 𝑒 ⊆ ( 0 ... 5 )
218 163 197 164 ltleii ⊢ 4 ≤ 5
219 elfz2nn0 ⊢ ( 4 ∈ ( 0 ... 5 ) ↔ ( 4 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 4 ≤ 5 ) )
220 35 45 218 219 mpbir3an ⊢ 4 ∈ ( 0 ... 5 )
221 prssi ⊢ ( ( 3 ∈ ( 0 ... 5 ) ∧ 4 ∈ ( 0 ... 5 ) ) → { 3 , 4 } ⊆ ( 0 ... 5 ) )
222 210 220 221 mp2an ⊢ { 3 , 4 } ⊆ ( 0 ... 5 )
223 sseq1 ⊢ ( 𝑒 = { 3 , 4 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 3 , 4 } ⊆ ( 0 ... 5 ) ) )
224 7 223 ralsn ⊢ ( ∀ 𝑒 ∈ { { 3 , 4 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ { 3 , 4 } ⊆ ( 0 ... 5 ) )
225 222 224 mpbir ⊢ ∀ 𝑒 ∈ { { 3 , 4 } } 𝑒 ⊆ ( 0 ... 5 )
226 ralunb ⊢ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) 𝑒 ⊆ ( 0 ... 5 ) ↔ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } 𝑒 ⊆ ( 0 ... 5 ) ∧ ∀ 𝑒 ∈ { { 3 , 4 } } 𝑒 ⊆ ( 0 ... 5 ) ) )
227 217 225 226 mpbir2an ⊢ ∀ 𝑒 ∈ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) 𝑒 ⊆ ( 0 ... 5 )
228 197 leidi ⊢ 5 ≤ 5
229 elfz2nn0 ⊢ ( 5 ∈ ( 0 ... 5 ) ↔ ( 5 ∈ ℕ0 ∧ 5 ∈ ℕ0 ∧ 5 ≤ 5 ) )
230 45 45 228 229 mpbir3an ⊢ 5 ∈ ( 0 ... 5 )
231 prssi ⊢ ( ( 4 ∈ ( 0 ... 5 ) ∧ 5 ∈ ( 0 ... 5 ) ) → { 4 , 5 } ⊆ ( 0 ... 5 ) )
232 220 230 231 mp2an ⊢ { 4 , 5 } ⊆ ( 0 ... 5 )
233 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 3 ∈ ( 0 ... 5 ) ) → { 0 , 3 } ⊆ ( 0 ... 5 ) )
234 196 210 233 mp2an ⊢ { 0 , 3 } ⊆ ( 0 ... 5 )
235 prssi ⊢ ( ( 0 ∈ ( 0 ... 5 ) ∧ 5 ∈ ( 0 ... 5 ) ) → { 0 , 5 } ⊆ ( 0 ... 5 ) )
236 196 230 235 mp2an ⊢ { 0 , 5 } ⊆ ( 0 ... 5 )
237 sseq1 ⊢ ( 𝑒 = { 4 , 5 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 4 , 5 } ⊆ ( 0 ... 5 ) ) )
238 sseq1 ⊢ ( 𝑒 = { 0 , 3 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 3 } ⊆ ( 0 ... 5 ) ) )
239 sseq1 ⊢ ( 𝑒 = { 0 , 5 } → ( 𝑒 ⊆ ( 0 ... 5 ) ↔ { 0 , 5 } ⊆ ( 0 ... 5 ) ) )
240 8 9 10 237 238 239 raltp ⊢ ( ∀ 𝑒 ∈ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } 𝑒 ⊆ ( 0 ... 5 ) ↔ ( { 4 , 5 } ⊆ ( 0 ... 5 ) ∧ { 0 , 3 } ⊆ ( 0 ... 5 ) ∧ { 0 , 5 } ⊆ ( 0 ... 5 ) ) )
241 232 234 236 240 mpbir3an ⊢ ∀ 𝑒 ∈ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } 𝑒 ⊆ ( 0 ... 5 )
242 ralunb ⊢ ( ∀ 𝑒 ∈ ( ( { { 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 ) ) )
243 227 241 242 mpbir2an ⊢ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ∪ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) 𝑒 ⊆ ( 0 ... 5 )
244 pwssb ⊢ ( ( ( { { 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 ) )
245 243 244 mpbir ⊢ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ∪ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ⊆ 𝒫 ( 0 ... 5 )
246 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( 0 ... 5 )
247 245 246 sseqtrri ⊢ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ∪ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ⊆ 𝒫 𝑉
248 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
249 1ex ⊢ 1 ∈ V
250 2ex ⊢ 2 ∈ V
251 249 250 75 3pm3.2i ⊢ ( 1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2 )
252 hashprb ⊢ ( ( 1 ∈ V ∧ 2 ∈ V ∧ 1 ≠ 2 ) ↔ ( ♯ ‘ { 1 , 2 } ) = 2 )
253 251 252 mpbi ⊢ ( ♯ ‘ { 1 , 2 } ) = 2
254 3ex ⊢ 3 ∈ V
255 250 254 106 3pm3.2i ⊢ ( 2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3 )
256 hashprb ⊢ ( ( 2 ∈ V ∧ 3 ∈ V ∧ 2 ≠ 3 ) ↔ ( ♯ ‘ { 2 , 3 } ) = 2 )
257 255 256 mpbi ⊢ ( ♯ ‘ { 2 , 3 } ) = 2
258 fveqeq2 ⊢ ( 𝑒 = { 0 , 1 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 1 } ) = 2 ) )
259 fveqeq2 ⊢ ( 𝑒 = { 1 , 2 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 1 , 2 } ) = 2 ) )
260 fveqeq2 ⊢ ( 𝑒 = { 2 , 3 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 2 , 3 } ) = 2 ) )
261 3 4 5 258 259 260 raltp ⊢ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 0 , 1 } ) = 2 ∧ ( ♯ ‘ { 1 , 2 } ) = 2 ∧ ( ♯ ‘ { 2 , 3 } ) = 2 ) )
262 248 253 257 261 mpbir3an ⊢ ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( ♯ ‘ 𝑒 ) = 2
263 35 elexi ⊢ 4 ∈ V
264 254 263 137 3pm3.2i ⊢ ( 3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4 )
265 hashprb ⊢ ( ( 3 ∈ V ∧ 4 ∈ V ∧ 3 ≠ 4 ) ↔ ( ♯ ‘ { 3 , 4 } ) = 2 )
266 264 265 mpbi ⊢ ( ♯ ‘ { 3 , 4 } ) = 2
267 fveqeq2 ⊢ ( 𝑒 = { 3 , 4 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 3 , 4 } ) = 2 ) )
268 7 267 ralsn ⊢ ( ∀ 𝑒 ∈ { { 3 , 4 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 3 , 4 } ) = 2 )
269 266 268 mpbir ⊢ ∀ 𝑒 ∈ { { 3 , 4 } } ( ♯ ‘ 𝑒 ) = 2
270 ralunb ⊢ ( ∀ 𝑒 ∈ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ( ♯ ‘ 𝑒 ) = 2 ↔ ( ∀ 𝑒 ∈ { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( ♯ ‘ 𝑒 ) = 2 ∧ ∀ 𝑒 ∈ { { 3 , 4 } } ( ♯ ‘ 𝑒 ) = 2 ) )
271 262 269 270 mpbir2an ⊢ ∀ 𝑒 ∈ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ( ♯ ‘ 𝑒 ) = 2
272 45 elexi ⊢ 5 ∈ V
273 263 272 165 3pm3.2i ⊢ ( 4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5 )
274 hashprb ⊢ ( ( 4 ∈ V ∧ 5 ∈ V ∧ 4 ≠ 5 ) ↔ ( ♯ ‘ { 4 , 5 } ) = 2 )
275 273 274 mpbi ⊢ ( ♯ ‘ { 4 , 5 } ) = 2
276 c0ex ⊢ 0 ∈ V
277 276 254 30 3pm3.2i ⊢ ( 0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3 )
278 hashprb ⊢ ( ( 0 ∈ V ∧ 3 ∈ V ∧ 0 ≠ 3 ) ↔ ( ♯ ‘ { 0 , 3 } ) = 2 )
279 277 278 mpbi ⊢ ( ♯ ‘ { 0 , 3 } ) = 2
280 276 272 49 3pm3.2i ⊢ ( 0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5 )
281 hashprb ⊢ ( ( 0 ∈ V ∧ 5 ∈ V ∧ 0 ≠ 5 ) ↔ ( ♯ ‘ { 0 , 5 } ) = 2 )
282 280 281 mpbi ⊢ ( ♯ ‘ { 0 , 5 } ) = 2
283 fveqeq2 ⊢ ( 𝑒 = { 4 , 5 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 4 , 5 } ) = 2 ) )
284 fveqeq2 ⊢ ( 𝑒 = { 0 , 3 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 3 } ) = 2 ) )
285 fveqeq2 ⊢ ( 𝑒 = { 0 , 5 } → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ { 0 , 5 } ) = 2 ) )
286 8 9 10 283 284 285 raltp ⊢ ( ∀ 𝑒 ∈ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ( ♯ ‘ 𝑒 ) = 2 ↔ ( ( ♯ ‘ { 4 , 5 } ) = 2 ∧ ( ♯ ‘ { 0 , 3 } ) = 2 ∧ ( ♯ ‘ { 0 , 5 } ) = 2 ) )
287 275 279 282 286 mpbir3an ⊢ ∀ 𝑒 ∈ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ( ♯ ‘ 𝑒 ) = 2
288 ralunb ⊢ ( ∀ 𝑒 ∈ ( ( { { 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 ) )
289 271 287 288 mpbir2an ⊢ ∀ 𝑒 ∈ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ∪ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ( ♯ ‘ 𝑒 ) = 2
290 ssrab ⊢ ( ( ( { { 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 ) )
291 247 289 290 mpbir2an ⊢ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } } ) ∪ { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
292 f1ss ⊢ ( ( 𝐸 : 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 } )
293 194 291 292 sylancl ⊢ ( ( ( ( ( { 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 } )
294 177 2 293 mp2an ⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }