Proof of Theorem xp11
Step | Hyp | Ref
| Expression |
1 | | xpnz 5045 |
. . 3
⊢ ((A ≠ ∅ ∧ B ≠ ∅) ↔ (A
× B) ≠ ∅) |
2 | | anidm 625 |
. . . . . 6
⊢ (((A × B)
≠ ∅ ∧
(A × B) ≠ ∅) ↔
(A × B) ≠ ∅) |
3 | | neeq1 2524 |
. . . . . . 7
⊢ ((A × B) =
(C × D) → ((A
× B) ≠ ∅ ↔ (C
× D) ≠ ∅)) |
4 | 3 | anbi2d 684 |
. . . . . 6
⊢ ((A × B) =
(C × D) → (((A
× B) ≠ ∅ ∧ (A × B)
≠ ∅) ↔ ((A × B)
≠ ∅ ∧
(C × D) ≠ ∅))) |
5 | 2, 4 | syl5bbr 250 |
. . . . 5
⊢ ((A × B) =
(C × D) → ((A
× B) ≠ ∅ ↔ ((A
× B) ≠ ∅ ∧ (C × D)
≠ ∅))) |
6 | | eqimss 3323 |
. . . . . . . 8
⊢ ((A × B) =
(C × D) → (A
× B) ⊆ (C ×
D)) |
7 | | ssxpb 5055 |
. . . . . . . 8
⊢ ((A × B)
≠ ∅ → ((A × B)
⊆ (C
× D) ↔ (A ⊆ C ∧ B ⊆ D))) |
8 | 6, 7 | syl5ibcom 211 |
. . . . . . 7
⊢ ((A × B) =
(C × D) → ((A
× B) ≠ ∅ → (A
⊆ C
∧ B ⊆ D))) |
9 | | eqimss2 3324 |
. . . . . . . 8
⊢ ((A × B) =
(C × D) → (C
× D) ⊆ (A ×
B)) |
10 | | ssxpb 5055 |
. . . . . . . 8
⊢ ((C × D)
≠ ∅ → ((C × D)
⊆ (A
× B) ↔ (C ⊆ A ∧ D ⊆ B))) |
11 | 9, 10 | syl5ibcom 211 |
. . . . . . 7
⊢ ((A × B) =
(C × D) → ((C
× D) ≠ ∅ → (C
⊆ A
∧ D ⊆ B))) |
12 | 8, 11 | anim12d 546 |
. . . . . 6
⊢ ((A × B) =
(C × D) → (((A
× B) ≠ ∅ ∧ (C × D)
≠ ∅) → ((A ⊆ C ∧ B ⊆ D) ∧ (C ⊆ A ∧ D ⊆ B)))) |
13 | | an4 797 |
. . . . . . 7
⊢ (((A ⊆ C ∧ B ⊆ D) ∧ (C ⊆ A ∧ D ⊆ B)) ↔ ((A
⊆ C
∧ C ⊆ A) ∧ (B ⊆ D ∧ D ⊆ B))) |
14 | | eqss 3287 |
. . . . . . . 8
⊢ (A = C ↔
(A ⊆
C ∧
C ⊆
A)) |
15 | | eqss 3287 |
. . . . . . . 8
⊢ (B = D ↔
(B ⊆
D ∧
D ⊆
B)) |
16 | 14, 15 | anbi12i 678 |
. . . . . . 7
⊢ ((A = C ∧ B = D) ↔ ((A
⊆ C
∧ C ⊆ A) ∧ (B ⊆ D ∧ D ⊆ B))) |
17 | 13, 16 | bitr4i 243 |
. . . . . 6
⊢ (((A ⊆ C ∧ B ⊆ D) ∧ (C ⊆ A ∧ D ⊆ B)) ↔ (A =
C ∧
B = D)) |
18 | 12, 17 | syl6ib 217 |
. . . . 5
⊢ ((A × B) =
(C × D) → (((A
× B) ≠ ∅ ∧ (C × D)
≠ ∅) → (A = C ∧ B = D))) |
19 | 5, 18 | sylbid 206 |
. . . 4
⊢ ((A × B) =
(C × D) → ((A
× B) ≠ ∅ → (A =
C ∧
B = D))) |
20 | 19 | com12 27 |
. . 3
⊢ ((A × B)
≠ ∅ → ((A × B) =
(C × D) → (A =
C ∧
B = D))) |
21 | 1, 20 | sylbi 187 |
. 2
⊢ ((A ≠ ∅ ∧ B ≠ ∅) → ((A
× B) = (C × D)
→ (A = C ∧ B = D))) |
22 | | xpeq12 4803 |
. 2
⊢ ((A = C ∧ B = D) → (A
× B) = (C × D)) |
23 | 21, 22 | impbid1 194 |
1
⊢ ((A ≠ ∅ ∧ B ≠ ∅) → ((A
× B) = (C × D)
↔ (A = C ∧ B = D))) |