Metamath Proof Explorer


Theorem xpima

Description: Direct image by a Cartesian product. (Contributed by Thierry Arnoux, 4-Feb-2017)

Ref Expression
Assertion xpima A×BC=ifAC=B

Proof

Step Hyp Ref Expression
1 exmid AC=¬AC=
2 df-ima A×BC=ranA×BC
3 df-res A×BC=A×BC×V
4 3 rneqi ranA×BC=ranA×BC×V
5 2 4 eqtri A×BC=ranA×BC×V
6 inxp A×BC×V=AC×BV
7 6 rneqi ranA×BC×V=ranAC×BV
8 inv1 BV=B
9 8 xpeq2i AC×BV=AC×B
10 9 rneqi ranAC×BV=ranAC×B
11 5 7 10 3eqtri A×BC=ranAC×B
12 xpeq1 AC=AC×B=×B
13 0xp ×B=
14 12 13 eqtrdi AC=AC×B=
15 14 rneqd AC=ranAC×B=ran
16 rn0 ran=
17 15 16 eqtrdi AC=ranAC×B=
18 11 17 eqtrid AC=A×BC=
19 18 ancli AC=AC=A×BC=
20 df-ne AC¬AC=
21 rnxp ACranAC×B=B
22 20 21 sylbir ¬AC=ranAC×B=B
23 11 22 eqtrid ¬AC=A×BC=B
24 23 ancli ¬AC=¬AC=A×BC=B
25 19 24 orim12i AC=¬AC=AC=A×BC=¬AC=A×BC=B
26 1 25 ax-mp AC=A×BC=¬AC=A×BC=B
27 eqif A×BC=ifAC=BAC=A×BC=¬AC=A×BC=B
28 26 27 mpbir A×BC=ifAC=B