Metamath Proof Explorer


Theorem coe1mul2lem2

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

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

Proof

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