Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 ) |
2 |
|
n0 |
⊢ ( 𝐵 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐵 ) |
3 |
1 2
|
anbi12i |
⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) ) |
4 |
|
exdistrv |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 𝑦 ∈ 𝐵 ) ) |
5 |
3 4
|
bitr4i |
⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) |
6 |
|
opex |
⊢ 〈 𝑥 , 𝑦 〉 ∈ V |
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 |
⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ ) |