Step |
Hyp |
Ref |
Expression |
1 |
|
coe1mul2lem2.h |
⊢ 𝐻 = { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑑 ∘r ≤ ( 1o × { 𝑘 } ) } |
2 |
|
df1o2 |
⊢ 1o = { ∅ } |
3 |
|
nn0ex |
⊢ ℕ0 ∈ V |
4 |
|
0ex |
⊢ ∅ ∈ V |
5 |
|
eqid |
⊢ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) = ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) |
6 |
2 3 4 5
|
mapsnf1o2 |
⊢ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 |
7 |
|
f1of1 |
⊢ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1→ ℕ0 ) |
8 |
6 7
|
ax-mp |
⊢ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1→ ℕ0 |
9 |
1
|
ssrab3 |
⊢ 𝐻 ⊆ ( ℕ0 ↑m 1o ) |
10 |
9
|
a1i |
⊢ ( 𝑘 ∈ ℕ0 → 𝐻 ⊆ ( ℕ0 ↑m 1o ) ) |
11 |
|
f1ores |
⊢ ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1→ ℕ0 ∧ 𝐻 ⊆ ( ℕ0 ↑m 1o ) ) → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) ) |
12 |
8 10 11
|
sylancr |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) ) |
13 |
|
coe1mul2lem1 |
⊢ ( ( 𝑘 ∈ ℕ0 ∧ 𝑑 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝑑 ∘r ≤ ( 1o × { 𝑘 } ) ↔ ( 𝑑 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) ) |
14 |
13
|
rabbidva |
⊢ ( 𝑘 ∈ ℕ0 → { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑑 ∘r ≤ ( 1o × { 𝑘 } ) } = { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ ( 𝑑 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) } ) |
15 |
|
fveq1 |
⊢ ( 𝑐 = 𝑑 → ( 𝑐 ‘ ∅ ) = ( 𝑑 ‘ ∅ ) ) |
16 |
15
|
eleq1d |
⊢ ( 𝑐 = 𝑑 → ( ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ↔ ( 𝑑 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) ) |
17 |
16
|
cbvrabv |
⊢ { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) } = { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ ( 𝑑 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) } |
18 |
14 17
|
eqtr4di |
⊢ ( 𝑘 ∈ ℕ0 → { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑑 ∘r ≤ ( 1o × { 𝑘 } ) } = { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) } ) |
19 |
5
|
mptpreima |
⊢ ( ◡ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( 0 ... 𝑘 ) ) = { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) } |
20 |
18 1 19
|
3eqtr4g |
⊢ ( 𝑘 ∈ ℕ0 → 𝐻 = ( ◡ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( 0 ... 𝑘 ) ) ) |
21 |
20
|
imaeq2d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) = ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( ◡ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( 0 ... 𝑘 ) ) ) ) |
22 |
|
f1ofo |
⊢ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 ) |
23 |
6 22
|
ax-mp |
⊢ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 |
24 |
|
fz0ssnn0 |
⊢ ( 0 ... 𝑘 ) ⊆ ℕ0 |
25 |
|
foimacnv |
⊢ ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 ∧ ( 0 ... 𝑘 ) ⊆ ℕ0 ) → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( ◡ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( 0 ... 𝑘 ) ) ) = ( 0 ... 𝑘 ) ) |
26 |
23 24 25
|
mp2an |
⊢ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( ◡ ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ ( 0 ... 𝑘 ) ) ) = ( 0 ... 𝑘 ) |
27 |
21 26
|
eqtrdi |
⊢ ( 𝑘 ∈ ℕ0 → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) = ( 0 ... 𝑘 ) ) |
28 |
27
|
f1oeq3d |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) ↔ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ) ) |
29 |
|
resmpt |
⊢ ( 𝐻 ⊆ ( ℕ0 ↑m 1o ) → ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) = ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) ) |
30 |
|
f1oeq1 |
⊢ ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) = ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) → ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ↔ ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ) ) |
31 |
10 29 30
|
3syl |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ↔ ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ) ) |
32 |
28 31
|
bitrd |
⊢ ( 𝑘 ∈ ℕ0 → ( ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) ↾ 𝐻 ) : 𝐻 –1-1-onto→ ( ( 𝑐 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑐 ‘ ∅ ) ) “ 𝐻 ) ↔ ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ) ) |
33 |
12 32
|
mpbid |
⊢ ( 𝑘 ∈ ℕ0 → ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) ) |