Step | Hyp | Ref
| Expression |
1 | | xpm 4688 |
. . . . . . . 8
⊢ ((∃𝑎 𝑎 ∈ A ∧ ∃𝑏 𝑏 ∈ B) ↔ ∃x x ∈ (A × B)) |
2 | | dmxpm 4498 |
. . . . . . . . 9
⊢ (∃𝑏 𝑏 ∈ B → dom (A
× B) = A) |
3 | 2 | adantl 262 |
. . . . . . . 8
⊢ ((∃𝑎 𝑎 ∈ A ∧ ∃𝑏 𝑏 ∈ B) → dom (A
× B) = A) |
4 | 1, 3 | sylbir 125 |
. . . . . . 7
⊢ (∃x x ∈ (A × B)
→ dom (A × B) = A) |
5 | 4 | adantr 261 |
. . . . . 6
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → dom (A × B) =
A) |
6 | | dmss 4477 |
. . . . . . 7
⊢
((A × B) ⊆ (𝐶 × 𝐷) → dom (A × B)
⊆ dom (𝐶 ×
𝐷)) |
7 | 6 | adantl 262 |
. . . . . 6
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → dom (A × B)
⊆ dom (𝐶 ×
𝐷)) |
8 | 5, 7 | eqsstr3d 2974 |
. . . . 5
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → A ⊆ dom (𝐶 × 𝐷)) |
9 | | dmxpss 4696 |
. . . . 5
⊢ dom
(𝐶 × 𝐷) ⊆ 𝐶 |
10 | 8, 9 | syl6ss 2951 |
. . . 4
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → A ⊆ 𝐶) |
11 | | rnxpm 4695 |
. . . . . . . . 9
⊢ (∃𝑎 𝑎 ∈ A → ran (A
× B) = B) |
12 | 11 | adantr 261 |
. . . . . . . 8
⊢ ((∃𝑎 𝑎 ∈ A ∧ ∃𝑏 𝑏 ∈ B) → ran (A
× B) = B) |
13 | 1, 12 | sylbir 125 |
. . . . . . 7
⊢ (∃x x ∈ (A × B)
→ ran (A × B) = B) |
14 | 13 | adantr 261 |
. . . . . 6
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → ran (A × B) =
B) |
15 | | rnss 4507 |
. . . . . . 7
⊢
((A × B) ⊆ (𝐶 × 𝐷) → ran (A × B)
⊆ ran (𝐶 ×
𝐷)) |
16 | 15 | adantl 262 |
. . . . . 6
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → ran (A × B)
⊆ ran (𝐶 ×
𝐷)) |
17 | 14, 16 | eqsstr3d 2974 |
. . . . 5
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → B ⊆ ran (𝐶 × 𝐷)) |
18 | | rnxpss 4697 |
. . . . 5
⊢ ran
(𝐶 × 𝐷) ⊆ 𝐷 |
19 | 17, 18 | syl6ss 2951 |
. . . 4
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → B ⊆ 𝐷) |
20 | 10, 19 | jca 290 |
. . 3
⊢ ((∃x x ∈ (A × B)
∧ (A
× B) ⊆ (𝐶 × 𝐷)) → (A ⊆ 𝐶 ∧ B ⊆ 𝐷)) |
21 | 20 | ex 108 |
. 2
⊢ (∃x x ∈ (A × B)
→ ((A × B) ⊆ (𝐶 × 𝐷) → (A ⊆ 𝐶 ∧ B ⊆ 𝐷))) |
22 | | xpss12 4388 |
. 2
⊢
((A ⊆ 𝐶 ∧ B ⊆ 𝐷) → (A × B)
⊆ (𝐶 × 𝐷)) |
23 | 21, 22 | impbid1 130 |
1
⊢ (∃x x ∈ (A × B)
→ ((A × B) ⊆ (𝐶 × 𝐷) ↔ (A ⊆ 𝐶 ∧ B ⊆ 𝐷))) |