Metamath Proof Explorer

Theorem usgrexmpl1lem

Description: Lemma for usgrexmpl1 . (Contributed by AV, 2-Aug-2025)

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

Proof

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