Step | Hyp | Ref
| Expression |
1 | | xpm 4688 |
. . 3
⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) ↔ ∃z z ∈ (A × B)) |
2 | | anidm 376 |
. . . . . 6
⊢ ((∃z z ∈ (A × B)
∧ ∃z z ∈ (A ×
B)) ↔ ∃z z ∈ (A × B)) |
3 | | eleq2 2098 |
. . . . . . . 8
⊢
((A × B) = (𝐶 × 𝐷) → (z ∈ (A × B)
↔ z ∈ (𝐶 × 𝐷))) |
4 | 3 | exbidv 1703 |
. . . . . . 7
⊢
((A × B) = (𝐶 × 𝐷) → (∃z z ∈ (A × B)
↔ ∃z z ∈ (𝐶 × 𝐷))) |
5 | 4 | anbi2d 437 |
. . . . . 6
⊢
((A × B) = (𝐶 × 𝐷) → ((∃z z ∈ (A × B)
∧ ∃z z ∈ (A ×
B)) ↔ (∃z z ∈ (A × B)
∧ ∃z z ∈ (𝐶 × 𝐷)))) |
6 | 2, 5 | syl5bbr 183 |
. . . . 5
⊢
((A × B) = (𝐶 × 𝐷) → (∃z z ∈ (A × B)
↔ (∃z z ∈ (A ×
B) ∧ ∃z z ∈ (𝐶 × 𝐷)))) |
7 | | eqimss 2991 |
. . . . . . . 8
⊢
((A × B) = (𝐶 × 𝐷) → (A × B)
⊆ (𝐶 × 𝐷)) |
8 | | ssxpbm 4699 |
. . . . . . . 8
⊢ (∃z z ∈ (A × B)
→ ((A × B) ⊆ (𝐶 × 𝐷) ↔ (A ⊆ 𝐶 ∧ B ⊆ 𝐷))) |
9 | 7, 8 | syl5ibcom 144 |
. . . . . . 7
⊢
((A × B) = (𝐶 × 𝐷) → (∃z z ∈ (A × B)
→ (A ⊆ 𝐶 ∧ B ⊆ 𝐷))) |
10 | | eqimss2 2992 |
. . . . . . . 8
⊢
((A × B) = (𝐶 × 𝐷) → (𝐶 × 𝐷) ⊆ (A × B)) |
11 | | ssxpbm 4699 |
. . . . . . . 8
⊢ (∃z z ∈ (𝐶 × 𝐷) → ((𝐶 × 𝐷) ⊆ (A × B)
↔ (𝐶 ⊆ A ∧ 𝐷 ⊆ B))) |
12 | 10, 11 | syl5ibcom 144 |
. . . . . . 7
⊢
((A × B) = (𝐶 × 𝐷) → (∃z z ∈ (𝐶 × 𝐷) → (𝐶 ⊆ A ∧ 𝐷 ⊆ B))) |
13 | 9, 12 | anim12d 318 |
. . . . . 6
⊢
((A × B) = (𝐶 × 𝐷) → ((∃z z ∈ (A × B)
∧ ∃z z ∈ (𝐶 × 𝐷)) → ((A ⊆ 𝐶 ∧ B ⊆ 𝐷) ∧ (𝐶 ⊆ A ∧ 𝐷 ⊆ B)))) |
14 | | an4 520 |
. . . . . . 7
⊢
(((A ⊆ 𝐶 ∧ B ⊆ 𝐷) ∧ (𝐶 ⊆ A ∧ 𝐷 ⊆ B)) ↔ ((A
⊆ 𝐶 ∧ 𝐶 ⊆ A) ∧ (B ⊆ 𝐷 ∧ 𝐷 ⊆ B))) |
15 | | eqss 2954 |
. . . . . . . 8
⊢ (A = 𝐶 ↔ (A ⊆ 𝐶 ∧ 𝐶 ⊆ A)) |
16 | | eqss 2954 |
. . . . . . . 8
⊢ (B = 𝐷 ↔ (B ⊆ 𝐷 ∧ 𝐷 ⊆ B)) |
17 | 15, 16 | anbi12i 433 |
. . . . . . 7
⊢
((A = 𝐶 ∧ B = 𝐷) ↔ ((A ⊆ 𝐶 ∧ 𝐶 ⊆ A) ∧ (B ⊆ 𝐷 ∧ 𝐷 ⊆ B))) |
18 | 14, 17 | bitr4i 176 |
. . . . . 6
⊢
(((A ⊆ 𝐶 ∧ B ⊆ 𝐷) ∧ (𝐶 ⊆ A ∧ 𝐷 ⊆ B)) ↔ (A =
𝐶 ∧ B = 𝐷)) |
19 | 13, 18 | syl6ib 150 |
. . . . 5
⊢
((A × B) = (𝐶 × 𝐷) → ((∃z z ∈ (A × B)
∧ ∃z z ∈ (𝐶 × 𝐷)) → (A = 𝐶 ∧ B = 𝐷))) |
20 | 6, 19 | sylbid 139 |
. . . 4
⊢
((A × B) = (𝐶 × 𝐷) → (∃z z ∈ (A × B)
→ (A = 𝐶 ∧ B = 𝐷))) |
21 | 20 | com12 27 |
. . 3
⊢ (∃z z ∈ (A × B)
→ ((A × B) = (𝐶 × 𝐷) → (A = 𝐶 ∧ B = 𝐷))) |
22 | 1, 21 | sylbi 114 |
. 2
⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) → ((A
× B) = (𝐶 × 𝐷) → (A = 𝐶 ∧ B = 𝐷))) |
23 | | xpeq12 4307 |
. 2
⊢
((A = 𝐶 ∧ B = 𝐷) → (A × B) =
(𝐶 × 𝐷)) |
24 | 22, 23 | impbid1 130 |
1
⊢ ((∃x x ∈ A ∧ ∃y y ∈ B) → ((A
× B) = (𝐶 × 𝐷) ↔ (A = 𝐶 ∧ B = 𝐷))) |