Description: Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | xpima | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmid | |
|
2 | df-ima | |
|
3 | df-res | |
|
4 | 3 | rneqi | |
5 | 2 4 | eqtri | |
6 | inxp | |
|
7 | 6 | rneqi | |
8 | inv1 | |
|
9 | 8 | xpeq2i | |
10 | 9 | rneqi | |
11 | 5 7 10 | 3eqtri | |
12 | xpeq1 | |
|
13 | 0xp | |
|
14 | 12 13 | eqtrdi | |
15 | 14 | rneqd | |
16 | rn0 | |
|
17 | 15 16 | eqtrdi | |
18 | 11 17 | eqtrid | |
19 | 18 | ancli | |
20 | df-ne | |
|
21 | rnxp | |
|
22 | 20 21 | sylbir | |
23 | 11 22 | eqtrid | |
24 | 23 | ancli | |
25 | 19 24 | orim12i | |
26 | 1 25 | ax-mp | |
27 | eqif | |
|
28 | 26 27 | mpbir | |