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 A B A × B

Proof

Step Hyp Ref Expression
1 n0 A x x A
2 n0 B y y B
3 1 2 anbi12i A B x x A y y B
4 exdistrv x y x A y B x x A y y B
5 3 4 bitr4i A B x y x A y B
6 opex x y V
7 eleq1 z = x y z A × B x y A × B
8 opelxp x y A × B x A y B
9 7 8 bitrdi z = x y z A × B x A y B
10 6 9 spcev x A y B z z A × B
11 n0 A × B z z A × B
12 10 11 sylibr x A y B A × B
13 12 exlimivv x y x A y B A × B
14 5 13 sylbi A B A × B
15 xpeq1 A = A × B = × B
16 0xp × B =
17 15 16 eqtrdi A = A × B =
18 17 necon3i A × B A
19 xpeq2 B = A × B = A ×
20 xp0 A × =
21 19 20 eqtrdi B = A × B =
22 21 necon3i A × B B
23 18 22 jca A × B A B
24 14 23 impbii A B A × B