Metamath Proof Explorer

Theorem coe1mul2lem2

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypothesis coe1mul2lem2.h ⊢ 𝐻 = { 𝑑 ∈ ( ℕ0 ↑m 1o ) ∣ 𝑑 ∘r ≤ ( 1o × { 𝑘 } ) }
Assertion coe1mul2lem2 ( 𝑘 ∈ ℕ0 → ( 𝑐 ∈ 𝐻 ↦ ( 𝑐 ‘ ∅ ) ) : 𝐻 –1-1-onto→ ( 0 ... 𝑘 ) )

Proof

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 ... 𝑘 ) )