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