Metamath Proof Explorer


Theorem xpnz

Description: The Cartesian product of nonempty classes is nonempty. (Variation of a theorem contributed by Raph Levien, 30-Jun-2006.) (Contributed by NM, 30-Jun-2006)

Ref Expression
Assertion xpnz ABA×B

Proof

Step Hyp Ref Expression
1 n0 AxxA
2 n0 ByyB
3 1 2 anbi12i ABxxAyyB
4 exdistrv xyxAyBxxAyyB
5 3 4 bitr4i ABxyxAyB
6 opex xyV
7 eleq1 z=xyzA×BxyA×B
8 opelxp xyA×BxAyB
9 7 8 bitrdi z=xyzA×BxAyB
10 6 9 spcev xAyBzzA×B
11 n0 A×BzzA×B
12 10 11 sylibr xAyBA×B
13 12 exlimivv xyxAyBA×B
14 5 13 sylbi ABA×B
15 xpeq1 A=A×B=×B
16 0xp ×B=
17 15 16 eqtrdi A=A×B=
18 17 necon3i A×BA
19 xpeq2 B=A×B=A×
20 xp0 A×=
21 19 20 eqtrdi B=A×B=
22 21 necon3i A×BB
23 18 22 jca A×BAB
24 14 23 impbii ABA×B