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 𝒫 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 V
5 prex 1 2 V
6 prex 2 0 V
7 prex 0 3 V
8 s4f1o 0 1 V 1 2 V 2 0 V 0 3 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 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 2 0 0 3
10 3 2 9 mp2 E : dom E 1-1 onto 0 1 1 2 2 0 0 3
11 f1of1 E : dom E 1-1 onto 0 1 1 2 2 0 0 3 E : dom E 1-1 0 1 1 2 2 0 0 3
12 id ran E 0 1 1 2 2 0 0 3 ran E 0 1 1 2 2 0 0 3
13 vex p V
14 13 elpr p 0 1 1 2 p = 0 1 p = 1 2
15 0nn0 0 0
16 4nn0 4 0
17 0re 0
18 4re 4
19 4pos 0 < 4
20 17 18 19 ltleii 0 4
21 elfz2nn0 0 0 4 0 0 4 0 0 4
22 15 16 20 21 mpbir3an 0 0 4
23 22 1 eleqtrri 0 V
24 1nn0 1 0
25 1re 1
26 1lt4 1 < 4
27 25 18 26 ltleii 1 4
28 elfz2nn0 1 0 4 1 0 4 0 1 4
29 24 16 27 28 mpbir3an 1 0 4
30 29 1 eleqtrri 1 V
31 prelpwi 0 V 1 V 0 1 𝒫 V
32 eleq1 p = 0 1 p 𝒫 V 0 1 𝒫 V
33 31 32 syl5ibrcom 0 V 1 V p = 0 1 p 𝒫 V
34 23 30 33 mp2an p = 0 1 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 𝒫 V p = 2
39 2nn0 2 0
40 2re 2
41 2lt4 2 < 4
42 40 18 41 ltleii 2 4
43 elfz2nn0 2 0 4 2 0 4 0 2 4
44 39 16 42 43 mpbir3an 2 0 4
45 44 1 eleqtrri 2 V
46 prelpwi 1 V 2 V 1 2 𝒫 V
47 eleq1 p = 1 2 p 𝒫 V 1 2 𝒫 V
48 46 47 syl5ibrcom 1 V 2 V p = 1 2 p 𝒫 V
49 30 45 48 mp2an p = 1 2 p 𝒫 V
50 fveq2 p = 1 2 p = 1 2
51 1ne2 1 2
52 1nn 1
53 2nn 2
54 hashprg 1 2 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 𝒫 V p = 2
59 38 58 jaoi p = 0 1 p = 1 2 p 𝒫 V p = 2
60 14 59 sylbi p 0 1 1 2 p 𝒫 V p = 2
61 13 elpr p 2 0 0 3 p = 2 0 p = 0 3
62 prelpwi 2 V 0 V 2 0 𝒫 V
63 eleq1 p = 2 0 p 𝒫 V 2 0 𝒫 V
64 62 63 syl5ibrcom 2 V 0 V p = 2 0 p 𝒫 V
65 45 23 64 mp2an p = 2 0 p 𝒫 V
66 fveq2 p = 2 0 p = 2 0
67 2ne0 2 0
68 2z 2
69 0z 0
70 hashprg 2 0 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 𝒫 V p = 2
75 3nn0 3 0
76 3re 3
77 3lt4 3 < 4
78 76 18 77 ltleii 3 4
79 elfz2nn0 3 0 4 3 0 4 0 3 4
80 75 16 78 79 mpbir3an 3 0 4
81 80 1 eleqtrri 3 V
82 prelpwi 0 V 3 V 0 3 𝒫 V
83 eleq1 p = 0 3 p 𝒫 V 0 3 𝒫 V
84 82 83 syl5ibrcom 0 V 3 V p = 0 3 p 𝒫 V
85 23 81 84 mp2an p = 0 3 p 𝒫 V
86 fveq2 p = 0 3 p = 0 3
87 3ne0 3 0
88 87 necomi 0 3
89 3z 3
90 hashprg 0 3 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 𝒫 V p = 2
95 74 94 jaoi p = 2 0 p = 0 3 p 𝒫 V p = 2
96 61 95 sylbi p 2 0 0 3 p 𝒫 V p = 2
97 60 96 jaoi p 0 1 1 2 p 2 0 0 3 p 𝒫 V p = 2
98 elun p 0 1 1 2 2 0 0 3 p 0 1 1 2 p 2 0 0 3
99 fveqeq2 e = p e = 2 p = 2
100 99 elrab p e 𝒫 V | e = 2 p 𝒫 V p = 2
101 97 98 100 3imtr4i p 0 1 1 2 2 0 0 3 p e 𝒫 V | e = 2
102 101 ssriv 0 1 1 2 2 0 0 3 e 𝒫 V | e = 2
103 12 102 sstrdi ran E 0 1 1 2 2 0 0 3 ran E e 𝒫 V | e = 2
104 103 anim2i E Fn dom E ran E 0 1 1 2 2 0 0 3 E Fn dom E ran E e 𝒫 V | e = 2
105 df-f E : dom E 0 1 1 2 2 0 0 3 E Fn dom E ran E 0 1 1 2 2 0 0 3
106 df-f E : dom E e 𝒫 V | e = 2 E Fn dom E ran E e 𝒫 V | e = 2
107 104 105 106 3imtr4i E : dom E 0 1 1 2 2 0 0 3 E : dom E e 𝒫 V | e = 2
108 107 anim1i E : dom E 0 1 1 2 2 0 0 3 x * y y E x E : dom E e 𝒫 V | e = 2 x * y y E x
109 dff12 E : dom E 1-1 0 1 1 2 2 0 0 3 E : dom E 0 1 1 2 2 0 0 3 x * y y E x
110 dff12 E : dom E 1-1 e 𝒫 V | e = 2 E : dom E e 𝒫 V | e = 2 x * y y E x
111 108 109 110 3imtr4i E : dom E 1-1 0 1 1 2 2 0 0 3 E : dom E 1-1 e 𝒫 V | e = 2
112 10 11 111 mp2b E : dom E 1-1 e 𝒫 V | e = 2