Metamath Proof Explorer


Theorem coe1mul2lem2

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

Ref Expression
Hypothesis coe1mul2lem2.h H = d 0 1 𝑜 | d f 1 𝑜 × k
Assertion coe1mul2lem2 k 0 c H c : H 1-1 onto 0 k

Proof

Step Hyp Ref Expression
1 coe1mul2lem2.h H = d 0 1 𝑜 | d f 1 𝑜 × k
2 df1o2 1 𝑜 =
3 nn0ex 0 V
4 0ex V
5 eqid c 0 1 𝑜 c = c 0 1 𝑜 c
6 2 3 4 5 mapsnf1o2 c 0 1 𝑜 c : 0 1 𝑜 1-1 onto 0
7 f1of1 c 0 1 𝑜 c : 0 1 𝑜 1-1 onto 0 c 0 1 𝑜 c : 0 1 𝑜 1-1 0
8 6 7 ax-mp c 0 1 𝑜 c : 0 1 𝑜 1-1 0
9 1 ssrab3 H 0 1 𝑜
10 9 a1i k 0 H 0 1 𝑜
11 f1ores c 0 1 𝑜 c : 0 1 𝑜 1-1 0 H 0 1 𝑜 c 0 1 𝑜 c H : H 1-1 onto c 0 1 𝑜 c H
12 8 10 11 sylancr k 0 c 0 1 𝑜 c H : H 1-1 onto c 0 1 𝑜 c H
13 coe1mul2lem1 k 0 d 0 1 𝑜 d f 1 𝑜 × k d 0 k
14 13 rabbidva k 0 d 0 1 𝑜 | d f 1 𝑜 × k = d 0 1 𝑜 | d 0 k
15 fveq1 c = d c = d
16 15 eleq1d c = d c 0 k d 0 k
17 16 cbvrabv c 0 1 𝑜 | c 0 k = d 0 1 𝑜 | d 0 k
18 14 17 eqtr4di k 0 d 0 1 𝑜 | d f 1 𝑜 × k = c 0 1 𝑜 | c 0 k
19 5 mptpreima c 0 1 𝑜 c -1 0 k = c 0 1 𝑜 | c 0 k
20 18 1 19 3eqtr4g k 0 H = c 0 1 𝑜 c -1 0 k
21 20 imaeq2d k 0 c 0 1 𝑜 c H = c 0 1 𝑜 c c 0 1 𝑜 c -1 0 k
22 f1ofo c 0 1 𝑜 c : 0 1 𝑜 1-1 onto 0 c 0 1 𝑜 c : 0 1 𝑜 onto 0
23 6 22 ax-mp c 0 1 𝑜 c : 0 1 𝑜 onto 0
24 fz0ssnn0 0 k 0
25 foimacnv c 0 1 𝑜 c : 0 1 𝑜 onto 0 0 k 0 c 0 1 𝑜 c c 0 1 𝑜 c -1 0 k = 0 k
26 23 24 25 mp2an c 0 1 𝑜 c c 0 1 𝑜 c -1 0 k = 0 k
27 21 26 eqtrdi k 0 c 0 1 𝑜 c H = 0 k
28 27 f1oeq3d k 0 c 0 1 𝑜 c H : H 1-1 onto c 0 1 𝑜 c H c 0 1 𝑜 c H : H 1-1 onto 0 k
29 resmpt H 0 1 𝑜 c 0 1 𝑜 c H = c H c
30 f1oeq1 c 0 1 𝑜 c H = c H c c 0 1 𝑜 c H : H 1-1 onto 0 k c H c : H 1-1 onto 0 k
31 10 29 30 3syl k 0 c 0 1 𝑜 c H : H 1-1 onto 0 k c H c : H 1-1 onto 0 k
32 28 31 bitrd k 0 c 0 1 𝑜 c H : H 1-1 onto c 0 1 𝑜 c H c H c : H 1-1 onto 0 k
33 12 32 mpbid k 0 c H c : H 1-1 onto 0 k