This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpl2lem

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

Ref Expression
Hypotheses usgrexmpl2.v 
|- V = ( 0 ... 5 )
usgrexmpl2.e 
|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
Assertion usgrexmpl2lem 
|- E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v 
 |-  V = ( 0 ... 5 )
2 usgrexmpl2.e 
 |-  E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ">
3 prex 
 |-  { 0 , 1 } e. _V
4 prex 
 |-  { 1 , 2 } e. _V
5 prex 
 |-  { 2 , 3 } e. _V
6 3 4 5 3pm3.2i 
 |-  ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V )
7 prex 
 |-  { 3 , 4 } e. _V
8 prex 
 |-  { 4 , 5 } e. _V
9 prex 
 |-  { 0 , 3 } e. _V
10 prex 
 |-  { 0 , 5 } e. _V
11 8 9 10 3pm3.2i 
 |-  ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _V )
12 6 7 11 3pm3.2i 
 |-  ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _V ) )
13 0nn0 
 |-  0 e. NN0
14 1nn0 
 |-  1 e. NN0
15 13 14 pm3.2i 
 |-  ( 0 e. NN0 /\ 1 e. NN0 )
16 2nn0 
 |-  2 e. NN0
17 14 16 pm3.2i 
 |-  ( 1 e. NN0 /\ 2 e. NN0 )
18 15 17 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 1 e. NN0 /\ 2 e. NN0 ) )
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 e. NN0 /\ 1 e. NN0 ) /\ ( 1 e. NN0 /\ 2 e. NN0 ) ) -> ( ( ( 0 =/= 1 /\ 0 =/= 2 ) \/ ( 1 =/= 1 /\ 1 =/= 2 ) ) -> { 0 , 1 } =/= { 1 , 2 } ) )
24 18 22 23 mp2 
 |-  { 0 , 1 } =/= { 1 , 2 }
25 3nn0 
 |-  3 e. NN0
26 16 25 pm3.2i 
 |-  ( 2 e. NN0 /\ 3 e. NN0 )
27 15 26 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 2 e. NN0 /\ 3 e. NN0 ) )
28 0re 
 |-  0 e. RR
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 e. NN0 /\ 1 e. NN0 ) /\ ( 2 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 0 =/= 2 /\ 0 =/= 3 ) \/ ( 1 =/= 2 /\ 1 =/= 3 ) ) -> { 0 , 1 } =/= { 2 , 3 } ) )
34 27 32 33 mp2 
 |-  { 0 , 1 } =/= { 2 , 3 }
35 4nn0 
 |-  4 e. NN0
36 25 35 pm3.2i 
 |-  ( 3 e. NN0 /\ 4 e. NN0 )
37 15 36 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) )
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 e. NN0 /\ 1 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) ) -> ( ( ( 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 e. NN0
46 35 45 pm3.2i 
 |-  ( 4 e. NN0 /\ 5 e. NN0 )
47 15 46 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
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 e. NN0 /\ 1 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 )
55 15 54 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) )
56 ax-1ne0 
 |-  1 =/= 0
57 1re 
 |-  1 e. RR
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 e. NN0 /\ 1 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 5 e. NN0 )
65 15 64 pm3.2i 
 |-  ( ( 0 e. NN0 /\ 1 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
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 e. NN0 /\ 1 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 2 e. NN0 ) /\ ( 2 e. NN0 /\ 3 e. NN0 ) )
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 e. NN0 /\ 2 e. NN0 ) /\ ( 2 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 2 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) )
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 e. NN0 /\ 2 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 2 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
89 82 67 pm3.2i 
 |-  ( 1 =/= 4 /\ 1 =/= 5 )
90 89 orci 
 |-  ( ( 1 =/= 4 /\ 1 =/= 5 ) \/ ( 2 =/= 4 /\ 2 =/= 5 ) )
91 prneimg 
 |-  ( ( ( 1 e. NN0 /\ 2 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 2 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) )
94 60 orci 
 |-  ( ( 1 =/= 0 /\ 1 =/= 3 ) \/ ( 2 =/= 0 /\ 2 =/= 3 ) )
95 prneimg 
 |-  ( ( ( 1 e. NN0 /\ 2 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 2 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
98 68 orci 
 |-  ( ( 1 =/= 0 /\ 1 =/= 5 ) \/ ( 2 =/= 0 /\ 2 =/= 5 ) )
99 prneimg 
 |-  ( ( ( 1 e. NN0 /\ 2 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) )
104 2re 
 |-  2 e. RR
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 e. NN0 /\ 3 e. NN0 ) /\ ( 3 e. NN0 /\ 4 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
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 e. NN0 /\ 3 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) )
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 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
127 121 115 pm3.2i 
 |-  ( 2 =/= 0 /\ 2 =/= 5 )
128 127 orci 
 |-  ( ( 2 =/= 0 /\ 2 =/= 5 ) \/ ( 3 =/= 0 /\ 3 =/= 5 ) )
129 prneimg 
 |-  ( ( ( 2 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 4 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) )
135 3re 
 |-  3 e. RR
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 e. NN0 /\ 4 e. NN0 ) /\ ( 4 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 4 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) )
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 e. NN0 /\ 4 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 4 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
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 e. NN0 /\ 4 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 5 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) )
159 147 orci 
 |-  ( ( 4 =/= 0 /\ 4 =/= 3 ) \/ ( 5 =/= 0 /\ 5 =/= 3 ) )
160 prneimg 
 |-  ( ( ( 4 e. NN0 /\ 5 e. NN0 ) /\ ( 0 e. NN0 /\ 3 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 5 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
163 4re 
 |-  4 e. RR
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 e. NN0 /\ 5 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) )
171 153 olci 
 |-  ( ( 0 =/= 0 /\ 0 =/= 5 ) \/ ( 3 =/= 0 /\ 3 =/= 5 ) )
172 prneimg 
 |-  ( ( ( 0 e. NN0 /\ 3 e. NN0 ) /\ ( 0 e. NN0 /\ 5 e. NN0 ) ) -> ( ( ( 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 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> -> E : ( 0 ..^ 7 ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ) )
179 178 imp 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) -> E : ( 0 ..^ 7 ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 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 ) -> ( E : ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) <-> E : ( 0 ..^ 7 ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ) )
183 181 182 ax-mp 
 |-  ( E : ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) <-> E : ( 0 ..^ 7 ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
184 179 183 sylibr 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) -> E : ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
185 2 dmeqi 
 |-  dom E = 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 } "> e. Word _V
187 wrddm 
 |-  ( <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> e. 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 E = ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) )
190 f1oeq2 
 |-  ( dom E = ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -> ( E : dom E -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) <-> E : ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ) )
191 189 190 ax-mp 
 |-  ( E : dom E -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) <-> E : ( 0 ..^ ( # ` <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) ) -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
192 184 191 sylibr 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) -> E : dom E -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
193 f1of1 
 |-  ( E : dom E -1-1-onto-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) -> E : dom E -1-1-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
194 192 193 syl 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) -> E : dom E -1-1-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) )
195 0elfz 
 |-  ( 5 e. NN0 -> 0 e. ( 0 ... 5 ) )
196 45 195 ax-mp 
 |-  0 e. ( 0 ... 5 )
197 5re 
 |-  5 e. RR
198 57 197 66 ltleii 
 |-  1 <_ 5
199 elfz2nn0 
 |-  ( 1 e. ( 0 ... 5 ) <-> ( 1 e. NN0 /\ 5 e. NN0 /\ 1 <_ 5 ) )
200 14 45 198 199 mpbir3an 
 |-  1 e. ( 0 ... 5 )
201 prssi 
 |-  ( ( 0 e. ( 0 ... 5 ) /\ 1 e. ( 0 ... 5 ) ) -> { 0 , 1 } C_ ( 0 ... 5 ) )
202 196 200 201 mp2an 
 |-  { 0 , 1 } C_ ( 0 ... 5 )
203 104 197 114 ltleii 
 |-  2 <_ 5
204 elfz2nn0 
 |-  ( 2 e. ( 0 ... 5 ) <-> ( 2 e. NN0 /\ 5 e. NN0 /\ 2 <_ 5 ) )
205 16 45 203 204 mpbir3an 
 |-  2 e. ( 0 ... 5 )
206 prssi 
 |-  ( ( 1 e. ( 0 ... 5 ) /\ 2 e. ( 0 ... 5 ) ) -> { 1 , 2 } C_ ( 0 ... 5 ) )
207 200 205 206 mp2an 
 |-  { 1 , 2 } C_ ( 0 ... 5 )
208 135 197 138 ltleii 
 |-  3 <_ 5
209 elfz2nn0 
 |-  ( 3 e. ( 0 ... 5 ) <-> ( 3 e. NN0 /\ 5 e. NN0 /\ 3 <_ 5 ) )
210 25 45 208 209 mpbir3an 
 |-  3 e. ( 0 ... 5 )
211 prssi 
 |-  ( ( 2 e. ( 0 ... 5 ) /\ 3 e. ( 0 ... 5 ) ) -> { 2 , 3 } C_ ( 0 ... 5 ) )
212 205 210 211 mp2an 
 |-  { 2 , 3 } C_ ( 0 ... 5 )
213 sseq1 
 |-  ( e = { 0 , 1 } -> ( e C_ ( 0 ... 5 ) <-> { 0 , 1 } C_ ( 0 ... 5 ) ) )
214 sseq1 
 |-  ( e = { 1 , 2 } -> ( e C_ ( 0 ... 5 ) <-> { 1 , 2 } C_ ( 0 ... 5 ) ) )
215 sseq1 
 |-  ( e = { 2 , 3 } -> ( e C_ ( 0 ... 5 ) <-> { 2 , 3 } C_ ( 0 ... 5 ) ) )
216 3 4 5 213 214 215 raltp 
 |-  ( A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } e C_ ( 0 ... 5 ) <-> ( { 0 , 1 } C_ ( 0 ... 5 ) /\ { 1 , 2 } C_ ( 0 ... 5 ) /\ { 2 , 3 } C_ ( 0 ... 5 ) ) )
217 202 207 212 216 mpbir3an 
 |-  A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } e C_ ( 0 ... 5 )
218 163 197 164 ltleii 
 |-  4 <_ 5
219 elfz2nn0 
 |-  ( 4 e. ( 0 ... 5 ) <-> ( 4 e. NN0 /\ 5 e. NN0 /\ 4 <_ 5 ) )
220 35 45 218 219 mpbir3an 
 |-  4 e. ( 0 ... 5 )
221 prssi 
 |-  ( ( 3 e. ( 0 ... 5 ) /\ 4 e. ( 0 ... 5 ) ) -> { 3 , 4 } C_ ( 0 ... 5 ) )
222 210 220 221 mp2an 
 |-  { 3 , 4 } C_ ( 0 ... 5 )
223 sseq1 
 |-  ( e = { 3 , 4 } -> ( e C_ ( 0 ... 5 ) <-> { 3 , 4 } C_ ( 0 ... 5 ) ) )
224 7 223 ralsn 
 |-  ( A. e e. { { 3 , 4 } } e C_ ( 0 ... 5 ) <-> { 3 , 4 } C_ ( 0 ... 5 ) )
225 222 224 mpbir 
 |-  A. e e. { { 3 , 4 } } e C_ ( 0 ... 5 )
226 ralunb 
 |-  ( A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) e C_ ( 0 ... 5 ) <-> ( A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } e C_ ( 0 ... 5 ) /\ A. e e. { { 3 , 4 } } e C_ ( 0 ... 5 ) ) )
227 217 225 226 mpbir2an 
 |-  A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) e C_ ( 0 ... 5 )
228 197 leidi 
 |-  5 <_ 5
229 elfz2nn0 
 |-  ( 5 e. ( 0 ... 5 ) <-> ( 5 e. NN0 /\ 5 e. NN0 /\ 5 <_ 5 ) )
230 45 45 228 229 mpbir3an 
 |-  5 e. ( 0 ... 5 )
231 prssi 
 |-  ( ( 4 e. ( 0 ... 5 ) /\ 5 e. ( 0 ... 5 ) ) -> { 4 , 5 } C_ ( 0 ... 5 ) )
232 220 230 231 mp2an 
 |-  { 4 , 5 } C_ ( 0 ... 5 )
233 prssi 
 |-  ( ( 0 e. ( 0 ... 5 ) /\ 3 e. ( 0 ... 5 ) ) -> { 0 , 3 } C_ ( 0 ... 5 ) )
234 196 210 233 mp2an 
 |-  { 0 , 3 } C_ ( 0 ... 5 )
235 prssi 
 |-  ( ( 0 e. ( 0 ... 5 ) /\ 5 e. ( 0 ... 5 ) ) -> { 0 , 5 } C_ ( 0 ... 5 ) )
236 196 230 235 mp2an 
 |-  { 0 , 5 } C_ ( 0 ... 5 )
237 sseq1 
 |-  ( e = { 4 , 5 } -> ( e C_ ( 0 ... 5 ) <-> { 4 , 5 } C_ ( 0 ... 5 ) ) )
238 sseq1 
 |-  ( e = { 0 , 3 } -> ( e C_ ( 0 ... 5 ) <-> { 0 , 3 } C_ ( 0 ... 5 ) ) )
239 sseq1 
 |-  ( e = { 0 , 5 } -> ( e C_ ( 0 ... 5 ) <-> { 0 , 5 } C_ ( 0 ... 5 ) ) )
240 8 9 10 237 238 239 raltp 
 |-  ( A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } e C_ ( 0 ... 5 ) <-> ( { 4 , 5 } C_ ( 0 ... 5 ) /\ { 0 , 3 } C_ ( 0 ... 5 ) /\ { 0 , 5 } C_ ( 0 ... 5 ) ) )
241 232 234 236 240 mpbir3an 
 |-  A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } e C_ ( 0 ... 5 )
242 ralunb 
 |-  ( A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) e C_ ( 0 ... 5 ) <-> ( A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) e C_ ( 0 ... 5 ) /\ A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } e C_ ( 0 ... 5 ) ) )
243 227 241 242 mpbir2an 
 |-  A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) e C_ ( 0 ... 5 )
244 pwssb 
 |-  ( ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ ~P ( 0 ... 5 ) <-> A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) e C_ ( 0 ... 5 ) )
245 243 244 mpbir 
 |-  ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ ~P ( 0 ... 5 )
246 1 pweqi 
 |-  ~P V = ~P ( 0 ... 5 )
247 245 246 sseqtrri 
 |-  ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ ~P V
248 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
249 1ex 
 |-  1 e. _V
250 2ex 
 |-  2 e. _V
251 249 250 75 3pm3.2i 
 |-  ( 1 e. _V /\ 2 e. _V /\ 1 =/= 2 )
252 hashprb 
 |-  ( ( 1 e. _V /\ 2 e. _V /\ 1 =/= 2 ) <-> ( # ` { 1 , 2 } ) = 2 )
253 251 252 mpbi 
 |-  ( # ` { 1 , 2 } ) = 2
254 3ex 
 |-  3 e. _V
255 250 254 106 3pm3.2i 
 |-  ( 2 e. _V /\ 3 e. _V /\ 2 =/= 3 )
256 hashprb 
 |-  ( ( 2 e. _V /\ 3 e. _V /\ 2 =/= 3 ) <-> ( # ` { 2 , 3 } ) = 2 )
257 255 256 mpbi 
 |-  ( # ` { 2 , 3 } ) = 2
258 fveqeq2 
 |-  ( e = { 0 , 1 } -> ( ( # ` e ) = 2 <-> ( # ` { 0 , 1 } ) = 2 ) )
259 fveqeq2 
 |-  ( e = { 1 , 2 } -> ( ( # ` e ) = 2 <-> ( # ` { 1 , 2 } ) = 2 ) )
260 fveqeq2 
 |-  ( e = { 2 , 3 } -> ( ( # ` e ) = 2 <-> ( # ` { 2 , 3 } ) = 2 ) )
261 3 4 5 258 259 260 raltp 
 |-  ( A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( # ` e ) = 2 <-> ( ( # ` { 0 , 1 } ) = 2 /\ ( # ` { 1 , 2 } ) = 2 /\ ( # ` { 2 , 3 } ) = 2 ) )
262 248 253 257 261 mpbir3an 
 |-  A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( # ` e ) = 2
263 35 elexi 
 |-  4 e. _V
264 254 263 137 3pm3.2i 
 |-  ( 3 e. _V /\ 4 e. _V /\ 3 =/= 4 )
265 hashprb 
 |-  ( ( 3 e. _V /\ 4 e. _V /\ 3 =/= 4 ) <-> ( # ` { 3 , 4 } ) = 2 )
266 264 265 mpbi 
 |-  ( # ` { 3 , 4 } ) = 2
267 fveqeq2 
 |-  ( e = { 3 , 4 } -> ( ( # ` e ) = 2 <-> ( # ` { 3 , 4 } ) = 2 ) )
268 7 267 ralsn 
 |-  ( A. e e. { { 3 , 4 } } ( # ` e ) = 2 <-> ( # ` { 3 , 4 } ) = 2 )
269 266 268 mpbir 
 |-  A. e e. { { 3 , 4 } } ( # ` e ) = 2
270 ralunb 
 |-  ( A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) ( # ` e ) = 2 <-> ( A. e e. { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ( # ` e ) = 2 /\ A. e e. { { 3 , 4 } } ( # ` e ) = 2 ) )
271 262 269 270 mpbir2an 
 |-  A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) ( # ` e ) = 2
272 45 elexi 
 |-  5 e. _V
273 263 272 165 3pm3.2i 
 |-  ( 4 e. _V /\ 5 e. _V /\ 4 =/= 5 )
274 hashprb 
 |-  ( ( 4 e. _V /\ 5 e. _V /\ 4 =/= 5 ) <-> ( # ` { 4 , 5 } ) = 2 )
275 273 274 mpbi 
 |-  ( # ` { 4 , 5 } ) = 2
276 c0ex 
 |-  0 e. _V
277 276 254 30 3pm3.2i 
 |-  ( 0 e. _V /\ 3 e. _V /\ 0 =/= 3 )
278 hashprb 
 |-  ( ( 0 e. _V /\ 3 e. _V /\ 0 =/= 3 ) <-> ( # ` { 0 , 3 } ) = 2 )
279 277 278 mpbi 
 |-  ( # ` { 0 , 3 } ) = 2
280 276 272 49 3pm3.2i 
 |-  ( 0 e. _V /\ 5 e. _V /\ 0 =/= 5 )
281 hashprb 
 |-  ( ( 0 e. _V /\ 5 e. _V /\ 0 =/= 5 ) <-> ( # ` { 0 , 5 } ) = 2 )
282 280 281 mpbi 
 |-  ( # ` { 0 , 5 } ) = 2
283 fveqeq2 
 |-  ( e = { 4 , 5 } -> ( ( # ` e ) = 2 <-> ( # ` { 4 , 5 } ) = 2 ) )
284 fveqeq2 
 |-  ( e = { 0 , 3 } -> ( ( # ` e ) = 2 <-> ( # ` { 0 , 3 } ) = 2 ) )
285 fveqeq2 
 |-  ( e = { 0 , 5 } -> ( ( # ` e ) = 2 <-> ( # ` { 0 , 5 } ) = 2 ) )
286 8 9 10 283 284 285 raltp 
 |-  ( A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ( # ` e ) = 2 <-> ( ( # ` { 4 , 5 } ) = 2 /\ ( # ` { 0 , 3 } ) = 2 /\ ( # ` { 0 , 5 } ) = 2 ) )
287 275 279 282 286 mpbir3an 
 |-  A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ( # ` e ) = 2
288 ralunb 
 |-  ( A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ( # ` e ) = 2 <-> ( A. e e. ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) ( # ` e ) = 2 /\ A. e e. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ( # ` e ) = 2 ) )
289 271 287 288 mpbir2an 
 |-  A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ( # ` e ) = 2
290 ssrab 
 |-  ( ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ { e e. ~P V | ( # ` e ) = 2 } <-> ( ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ ~P V /\ A. e e. ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) ( # ` e ) = 2 ) )
291 247 289 290 mpbir2an 
 |-  ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ { e e. ~P V | ( # ` e ) = 2 }
292 f1ss 
 |-  ( ( E : dom E -1-1-> ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) /\ ( ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } u. { { 3 , 4 } } ) u. { { 4 , 5 } , { 0 , 3 } , { 0 , 5 } } ) C_ { e e. ~P V | ( # ` e ) = 2 } ) -> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
293 194 291 292 sylancl 
 |-  ( ( ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V /\ { 2 , 3 } e. _V ) /\ { 3 , 4 } e. _V /\ ( { 4 , 5 } e. _V /\ { 0 , 3 } e. _V /\ { 0 , 5 } e. _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 } ) ) ) ) /\ E = <" { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } "> ) -> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
294 177 2 293 mp2an 
 |-  E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }