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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | n0 | |
|
2 | n0 | |
|
3 | 1 2 | anbi12i | |
4 | exdistrv | |
|
5 | 3 4 | bitr4i | |
6 | opex | |
|
7 | eleq1 | |
|
8 | opelxp | |
|
9 | 7 8 | bitrdi | |
10 | 6 9 | spcev | |
11 | n0 | |
|
12 | 10 11 | sylibr | |
13 | 12 | exlimivv | |
14 | 5 13 | sylbi | |
15 | xpeq1 | |
|
16 | 0xp | |
|
17 | 15 16 | eqtrdi | |
18 | 17 | necon3i | |
19 | xpeq2 | |
|
20 | xp0 | |
|
21 | 19 20 | eqtrdi | |
22 | 21 | necon3i | |
23 | 18 22 | jca | |
24 | 14 23 | impbii | |