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

Metamath Proof Explorer

Theorem usgrexmplef

Description: Lemma for usgrexmpl . (Contributed by Alexander van der Vekens, 15-Aug-2017)

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

Proof

Step Hyp Ref Expression
1 usgrexmplef.v 
 |-  V = ( 0 ... 4 )
2 usgrexmplef.e 
 |-  E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
3 usgrexmpldifpr 
 |-  ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) )
4 prex 
 |-  { 0 , 1 } e. _V
5 prex 
 |-  { 1 , 2 } e. _V
6 prex 
 |-  { 2 , 0 } e. _V
7 prex 
 |-  { 0 , 3 } e. _V
8 s4f1o 
 |-  ( ( ( { 0 , 1 } e. _V /\ { 1 , 2 } e. _V ) /\ ( { 2 , 0 } e. _V /\ { 0 , 3 } e. _V ) ) -> ( ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) ) )
9 4 5 6 7 8 mp4an 
 |-  ( ( ( { 0 , 1 } =/= { 1 , 2 } /\ { 0 , 1 } =/= { 2 , 0 } /\ { 0 , 1 } =/= { 0 , 3 } ) /\ ( { 1 , 2 } =/= { 2 , 0 } /\ { 1 , 2 } =/= { 0 , 3 } /\ { 2 , 0 } =/= { 0 , 3 } ) ) -> ( E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } "> -> E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) )
10 3 2 9 mp2 
 |-  E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } )
11 f1of1 
 |-  ( E : dom E -1-1-onto-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
12 id 
 |-  ( ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) )
13 vex 
 |-  p e. _V
14 13 elpr 
 |-  ( p e. { { 0 , 1 } , { 1 , 2 } } <-> ( p = { 0 , 1 } \/ p = { 1 , 2 } ) )
15 0nn0 
 |-  0 e. NN0
16 4nn0 
 |-  4 e. NN0
17 0re 
 |-  0 e. RR
18 4re 
 |-  4 e. RR
19 4pos 
 |-  0 < 4
20 17 18 19 ltleii 
 |-  0 <_ 4
21 elfz2nn0 
 |-  ( 0 e. ( 0 ... 4 ) <-> ( 0 e. NN0 /\ 4 e. NN0 /\ 0 <_ 4 ) )
22 15 16 20 21 mpbir3an 
 |-  0 e. ( 0 ... 4 )
23 22 1 eleqtrri 
 |-  0 e. V
24 1nn0 
 |-  1 e. NN0
25 1re 
 |-  1 e. RR
26 1lt4 
 |-  1 < 4
27 25 18 26 ltleii 
 |-  1 <_ 4
28 elfz2nn0 
 |-  ( 1 e. ( 0 ... 4 ) <-> ( 1 e. NN0 /\ 4 e. NN0 /\ 1 <_ 4 ) )
29 24 16 27 28 mpbir3an 
 |-  1 e. ( 0 ... 4 )
30 29 1 eleqtrri 
 |-  1 e. V
31 prelpwi 
 |-  ( ( 0 e. V /\ 1 e. V ) -> { 0 , 1 } e. ~P V )
32 eleq1 
 |-  ( p = { 0 , 1 } -> ( p e. ~P V <-> { 0 , 1 } e. ~P V ) )
33 31 32 syl5ibrcom 
 |-  ( ( 0 e. V /\ 1 e. V ) -> ( p = { 0 , 1 } -> p e. ~P V ) )
34 23 30 33 mp2an 
 |-  ( p = { 0 , 1 } -> p e. ~P V )
35 fveq2 
 |-  ( p = { 0 , 1 } -> ( # ` p ) = ( # ` { 0 , 1 } ) )
36 prhash2ex 
 |-  ( # ` { 0 , 1 } ) = 2
37 35 36 eqtrdi 
 |-  ( p = { 0 , 1 } -> ( # ` p ) = 2 )
38 34 37 jca 
 |-  ( p = { 0 , 1 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
39 2nn0 
 |-  2 e. NN0
40 2re 
 |-  2 e. RR
41 2lt4 
 |-  2 < 4
42 40 18 41 ltleii 
 |-  2 <_ 4
43 elfz2nn0 
 |-  ( 2 e. ( 0 ... 4 ) <-> ( 2 e. NN0 /\ 4 e. NN0 /\ 2 <_ 4 ) )
44 39 16 42 43 mpbir3an 
 |-  2 e. ( 0 ... 4 )
45 44 1 eleqtrri 
 |-  2 e. V
46 prelpwi 
 |-  ( ( 1 e. V /\ 2 e. V ) -> { 1 , 2 } e. ~P V )
47 eleq1 
 |-  ( p = { 1 , 2 } -> ( p e. ~P V <-> { 1 , 2 } e. ~P V ) )
48 46 47 syl5ibrcom 
 |-  ( ( 1 e. V /\ 2 e. V ) -> ( p = { 1 , 2 } -> p e. ~P V ) )
49 30 45 48 mp2an 
 |-  ( p = { 1 , 2 } -> p e. ~P V )
50 fveq2 
 |-  ( p = { 1 , 2 } -> ( # ` p ) = ( # ` { 1 , 2 } ) )
51 1ne2 
 |-  1 =/= 2
52 1nn 
 |-  1 e. NN
53 2nn 
 |-  2 e. NN
54 hashprg 
 |-  ( ( 1 e. NN /\ 2 e. NN ) -> ( 1 =/= 2 <-> ( # ` { 1 , 2 } ) = 2 ) )
55 52 53 54 mp2an 
 |-  ( 1 =/= 2 <-> ( # ` { 1 , 2 } ) = 2 )
56 51 55 mpbi 
 |-  ( # ` { 1 , 2 } ) = 2
57 50 56 eqtrdi 
 |-  ( p = { 1 , 2 } -> ( # ` p ) = 2 )
58 49 57 jca 
 |-  ( p = { 1 , 2 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
59 38 58 jaoi 
 |-  ( ( p = { 0 , 1 } \/ p = { 1 , 2 } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
60 14 59 sylbi 
 |-  ( p e. { { 0 , 1 } , { 1 , 2 } } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
61 13 elpr 
 |-  ( p e. { { 2 , 0 } , { 0 , 3 } } <-> ( p = { 2 , 0 } \/ p = { 0 , 3 } ) )
62 prelpwi 
 |-  ( ( 2 e. V /\ 0 e. V ) -> { 2 , 0 } e. ~P V )
63 eleq1 
 |-  ( p = { 2 , 0 } -> ( p e. ~P V <-> { 2 , 0 } e. ~P V ) )
64 62 63 syl5ibrcom 
 |-  ( ( 2 e. V /\ 0 e. V ) -> ( p = { 2 , 0 } -> p e. ~P V ) )
65 45 23 64 mp2an 
 |-  ( p = { 2 , 0 } -> p e. ~P V )
66 fveq2 
 |-  ( p = { 2 , 0 } -> ( # ` p ) = ( # ` { 2 , 0 } ) )
67 2ne0 
 |-  2 =/= 0
68 2z 
 |-  2 e. ZZ
69 0z 
 |-  0 e. ZZ
70 hashprg 
 |-  ( ( 2 e. ZZ /\ 0 e. ZZ ) -> ( 2 =/= 0 <-> ( # ` { 2 , 0 } ) = 2 ) )
71 68 69 70 mp2an 
 |-  ( 2 =/= 0 <-> ( # ` { 2 , 0 } ) = 2 )
72 67 71 mpbi 
 |-  ( # ` { 2 , 0 } ) = 2
73 66 72 eqtrdi 
 |-  ( p = { 2 , 0 } -> ( # ` p ) = 2 )
74 65 73 jca 
 |-  ( p = { 2 , 0 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
75 3nn0 
 |-  3 e. NN0
76 3re 
 |-  3 e. RR
77 3lt4 
 |-  3 < 4
78 76 18 77 ltleii 
 |-  3 <_ 4
79 elfz2nn0 
 |-  ( 3 e. ( 0 ... 4 ) <-> ( 3 e. NN0 /\ 4 e. NN0 /\ 3 <_ 4 ) )
80 75 16 78 79 mpbir3an 
 |-  3 e. ( 0 ... 4 )
81 80 1 eleqtrri 
 |-  3 e. V
82 prelpwi 
 |-  ( ( 0 e. V /\ 3 e. V ) -> { 0 , 3 } e. ~P V )
83 eleq1 
 |-  ( p = { 0 , 3 } -> ( p e. ~P V <-> { 0 , 3 } e. ~P V ) )
84 82 83 syl5ibrcom 
 |-  ( ( 0 e. V /\ 3 e. V ) -> ( p = { 0 , 3 } -> p e. ~P V ) )
85 23 81 84 mp2an 
 |-  ( p = { 0 , 3 } -> p e. ~P V )
86 fveq2 
 |-  ( p = { 0 , 3 } -> ( # ` p ) = ( # ` { 0 , 3 } ) )
87 3ne0 
 |-  3 =/= 0
88 87 necomi 
 |-  0 =/= 3
89 3z 
 |-  3 e. ZZ
90 hashprg 
 |-  ( ( 0 e. ZZ /\ 3 e. ZZ ) -> ( 0 =/= 3 <-> ( # ` { 0 , 3 } ) = 2 ) )
91 69 89 90 mp2an 
 |-  ( 0 =/= 3 <-> ( # ` { 0 , 3 } ) = 2 )
92 88 91 mpbi 
 |-  ( # ` { 0 , 3 } ) = 2
93 86 92 eqtrdi 
 |-  ( p = { 0 , 3 } -> ( # ` p ) = 2 )
94 85 93 jca 
 |-  ( p = { 0 , 3 } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
95 74 94 jaoi 
 |-  ( ( p = { 2 , 0 } \/ p = { 0 , 3 } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
96 61 95 sylbi 
 |-  ( p e. { { 2 , 0 } , { 0 , 3 } } -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
97 60 96 jaoi 
 |-  ( ( p e. { { 0 , 1 } , { 1 , 2 } } \/ p e. { { 2 , 0 } , { 0 , 3 } } ) -> ( p e. ~P V /\ ( # ` p ) = 2 ) )
98 elun 
 |-  ( p e. ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( p e. { { 0 , 1 } , { 1 , 2 } } \/ p e. { { 2 , 0 } , { 0 , 3 } } ) )
99 fveqeq2 
 |-  ( e = p -> ( ( # ` e ) = 2 <-> ( # ` p ) = 2 ) )
100 99 elrab 
 |-  ( p e. { e e. ~P V | ( # ` e ) = 2 } <-> ( p e. ~P V /\ ( # ` p ) = 2 ) )
101 97 98 100 3imtr4i 
 |-  ( p e. ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> p e. { e e. ~P V | ( # ` e ) = 2 } )
102 101 ssriv 
 |-  ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) C_ { e e. ~P V | ( # ` e ) = 2 }
103 12 102 sstrdi 
 |-  ( ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> ran E C_ { e e. ~P V | ( # ` e ) = 2 } )
104 103 anim2i 
 |-  ( ( E Fn dom E /\ ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) -> ( E Fn dom E /\ ran E C_ { e e. ~P V | ( # ` e ) = 2 } ) )
105 df-f 
 |-  ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( E Fn dom E /\ ran E C_ ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) ) )
106 df-f 
 |-  ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } <-> ( E Fn dom E /\ ran E C_ { e e. ~P V | ( # ` e ) = 2 } ) )
107 104 105 106 3imtr4i 
 |-  ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E --> { e e. ~P V | ( # ` e ) = 2 } )
108 107 anim1i 
 |-  ( ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) /\ A. x E* y y E x ) -> ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } /\ A. x E* y y E x ) )
109 dff12 
 |-  ( E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) <-> ( E : dom E --> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) /\ A. x E* y y E x ) )
110 dff12 
 |-  ( E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } <-> ( E : dom E --> { e e. ~P V | ( # ` e ) = 2 } /\ A. x E* y y E x ) )
111 108 109 110 3imtr4i 
 |-  ( E : dom E -1-1-> ( { { 0 , 1 } , { 1 , 2 } } u. { { 2 , 0 } , { 0 , 3 } } ) -> E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 } )
112 10 11 111 mp2b 
 |-  E : dom E -1-1-> { e e. ~P V | ( # ` e ) = 2 }