Metamath Proof Explorer

Theorem usgrexmplef

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

Ref Expression
Hypotheses usgrexmplef.v ⊢ 𝑉 = ( 0 ... 4 )
usgrexmplef.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
Assertion usgrexmplef 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }

Proof

Step Hyp Ref Expression
1 usgrexmplef.v ⊢ 𝑉 = ( 0 ... 4 )
2 usgrexmplef.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 } ) ) → ( 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ → 𝐸 : dom 𝐸 –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 } ) ) → ( 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ → 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ) )
10 3 2 9 mp2 ⊢ 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } )
11 f1of1 ⊢ ( 𝐸 : dom 𝐸 –1-1-onto→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → 𝐸 : dom 𝐸 –1-1→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) )
12 id ⊢ ( ran 𝐸 ⊆ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → ran 𝐸 ⊆ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) )
13 vex ⊢ 𝑝 ∈ V
14 13 elpr ⊢ ( 𝑝 ∈ { { 0 , 1 } , { 1 , 2 } } ↔ ( 𝑝 = { 0 , 1 } ∨ 𝑝 = { 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 ∈ 𝑉
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 ∈ 𝑉
31 prelpwi ⊢ ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → { 0 , 1 } ∈ 𝒫 𝑉 )
32 eleq1 ⊢ ( 𝑝 = { 0 , 1 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 0 , 1 } ∈ 𝒫 𝑉 ) )
33 31 32 syl5ibrcom ⊢ ( ( 0 ∈ 𝑉 ∧ 1 ∈ 𝑉 ) → ( 𝑝 = { 0 , 1 } → 𝑝 ∈ 𝒫 𝑉 ) )
34 23 30 33 mp2an ⊢ ( 𝑝 = { 0 , 1 } → 𝑝 ∈ 𝒫 𝑉 )
35 fveq2 ⊢ ( 𝑝 = { 0 , 1 } → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ { 0 , 1 } ) )
36 prhash2ex ⊢ ( ♯ ‘ { 0 , 1 } ) = 2
37 35 36 eqtrdi ⊢ ( 𝑝 = { 0 , 1 } → ( ♯ ‘ 𝑝 ) = 2 )
38 34 37 jca ⊢ ( 𝑝 = { 0 , 1 } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 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 ∈ 𝑉
46 prelpwi ⊢ ( ( 1 ∈ 𝑉 ∧ 2 ∈ 𝑉 ) → { 1 , 2 } ∈ 𝒫 𝑉 )
47 eleq1 ⊢ ( 𝑝 = { 1 , 2 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 1 , 2 } ∈ 𝒫 𝑉 ) )
48 46 47 syl5ibrcom ⊢ ( ( 1 ∈ 𝑉 ∧ 2 ∈ 𝑉 ) → ( 𝑝 = { 1 , 2 } → 𝑝 ∈ 𝒫 𝑉 ) )
49 30 45 48 mp2an ⊢ ( 𝑝 = { 1 , 2 } → 𝑝 ∈ 𝒫 𝑉 )
50 fveq2 ⊢ ( 𝑝 = { 1 , 2 } → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ { 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 ⊢ ( 𝑝 = { 1 , 2 } → ( ♯ ‘ 𝑝 ) = 2 )
58 49 57 jca ⊢ ( 𝑝 = { 1 , 2 } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
59 38 58 jaoi ⊢ ( ( 𝑝 = { 0 , 1 } ∨ 𝑝 = { 1 , 2 } ) → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
60 14 59 sylbi ⊢ ( 𝑝 ∈ { { 0 , 1 } , { 1 , 2 } } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
61 13 elpr ⊢ ( 𝑝 ∈ { { 2 , 0 } , { 0 , 3 } } ↔ ( 𝑝 = { 2 , 0 } ∨ 𝑝 = { 0 , 3 } ) )
62 prelpwi ⊢ ( ( 2 ∈ 𝑉 ∧ 0 ∈ 𝑉 ) → { 2 , 0 } ∈ 𝒫 𝑉 )
63 eleq1 ⊢ ( 𝑝 = { 2 , 0 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 2 , 0 } ∈ 𝒫 𝑉 ) )
64 62 63 syl5ibrcom ⊢ ( ( 2 ∈ 𝑉 ∧ 0 ∈ 𝑉 ) → ( 𝑝 = { 2 , 0 } → 𝑝 ∈ 𝒫 𝑉 ) )
65 45 23 64 mp2an ⊢ ( 𝑝 = { 2 , 0 } → 𝑝 ∈ 𝒫 𝑉 )
66 fveq2 ⊢ ( 𝑝 = { 2 , 0 } → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ { 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 ⊢ ( 𝑝 = { 2 , 0 } → ( ♯ ‘ 𝑝 ) = 2 )
74 65 73 jca ⊢ ( 𝑝 = { 2 , 0 } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 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 ∈ 𝑉
82 prelpwi ⊢ ( ( 0 ∈ 𝑉 ∧ 3 ∈ 𝑉 ) → { 0 , 3 } ∈ 𝒫 𝑉 )
83 eleq1 ⊢ ( 𝑝 = { 0 , 3 } → ( 𝑝 ∈ 𝒫 𝑉 ↔ { 0 , 3 } ∈ 𝒫 𝑉 ) )
84 82 83 syl5ibrcom ⊢ ( ( 0 ∈ 𝑉 ∧ 3 ∈ 𝑉 ) → ( 𝑝 = { 0 , 3 } → 𝑝 ∈ 𝒫 𝑉 ) )
85 23 81 84 mp2an ⊢ ( 𝑝 = { 0 , 3 } → 𝑝 ∈ 𝒫 𝑉 )
86 fveq2 ⊢ ( 𝑝 = { 0 , 3 } → ( ♯ ‘ 𝑝 ) = ( ♯ ‘ { 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 ⊢ ( 𝑝 = { 0 , 3 } → ( ♯ ‘ 𝑝 ) = 2 )
94 85 93 jca ⊢ ( 𝑝 = { 0 , 3 } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
95 74 94 jaoi ⊢ ( ( 𝑝 = { 2 , 0 } ∨ 𝑝 = { 0 , 3 } ) → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
96 61 95 sylbi ⊢ ( 𝑝 ∈ { { 2 , 0 } , { 0 , 3 } } → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
97 60 96 jaoi ⊢ ( ( 𝑝 ∈ { { 0 , 1 } , { 1 , 2 } } ∨ 𝑝 ∈ { { 2 , 0 } , { 0 , 3 } } ) → ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
98 elun ⊢ ( 𝑝 ∈ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ↔ ( 𝑝 ∈ { { 0 , 1 } , { 1 , 2 } } ∨ 𝑝 ∈ { { 2 , 0 } , { 0 , 3 } } ) )
99 fveqeq2 ⊢ ( 𝑒 = 𝑝 → ( ( ♯ ‘ 𝑒 ) = 2 ↔ ( ♯ ‘ 𝑝 ) = 2 ) )
100 99 elrab ⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( 𝑝 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑝 ) = 2 ) )
101 97 98 100 3imtr4i ⊢ ( 𝑝 ∈ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
102 101 ssriv ⊢ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
103 12 102 sstrdi ⊢ ( ran 𝐸 ⊆ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → ran 𝐸 ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
104 103 anim2i ⊢ ( ( 𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ) → ( 𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
105 df-f ⊢ ( 𝐸 : dom 𝐸 ⟶ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ↔ ( 𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ) )
106 df-f ⊢ ( 𝐸 : dom 𝐸 ⟶ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( 𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
107 104 105 106 3imtr4i ⊢ ( 𝐸 : dom 𝐸 ⟶ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → 𝐸 : dom 𝐸 ⟶ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
108 107 anim1i ⊢ ( ( 𝐸 : dom 𝐸 ⟶ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑦 𝐸 𝑥 ) → ( 𝐸 : dom 𝐸 ⟶ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ∧ ∀ 𝑥 ∃* 𝑦 𝑦 𝐸 𝑥 ) )
109 dff12 ⊢ ( 𝐸 : dom 𝐸 –1-1→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ↔ ( 𝐸 : dom 𝐸 ⟶ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) ∧ ∀ 𝑥 ∃* 𝑦 𝑦 𝐸 𝑥 ) )
110 dff12 ⊢ ( 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( 𝐸 : dom 𝐸 ⟶ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ∧ ∀ 𝑥 ∃* 𝑦 𝑦 𝐸 𝑥 ) )
111 108 109 110 3imtr4i ⊢ ( 𝐸 : dom 𝐸 –1-1→ ( { { 0 , 1 } , { 1 , 2 } } ∪ { { 2 , 0 } , { 0 , 3 } } ) → 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
112 10 11 111 mp2b ⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }