Proof of Theorem ssxpb
Step | Hyp | Ref
| Expression |
1 | | xpnz 6062 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) |
2 | | dmxp 5838 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
3 | 2 | adantl 482 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → dom (𝐴 × 𝐵) = 𝐴) |
4 | 1, 3 | sylbir 234 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
5 | 4 | adantr 481 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) = 𝐴) |
6 | | dmss 5811 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
7 | 6 | adantl 482 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
8 | 5, 7 | eqsstrrd 3960 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ dom (𝐶 × 𝐷)) |
9 | | dmxpss 6074 |
. . . . 5
⊢ dom
(𝐶 × 𝐷) ⊆ 𝐶 |
10 | 8, 9 | sstrdi 3933 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ 𝐶) |
11 | | rnxp 6073 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
12 | 11 | adantr 481 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ran (𝐴 × 𝐵) = 𝐵) |
13 | 1, 12 | sylbir 234 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
14 | 13 | adantr 481 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) = 𝐵) |
15 | | rnss 5848 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
16 | 15 | adantl 482 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
17 | 14, 16 | eqsstrrd 3960 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ ran (𝐶 × 𝐷)) |
18 | | rnxpss 6075 |
. . . . 5
⊢ ran
(𝐶 × 𝐷) ⊆ 𝐷 |
19 | 17, 18 | sstrdi 3933 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ 𝐷) |
20 | 10, 19 | jca 512 |
. . 3
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)) |
21 | 20 | ex 413 |
. 2
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
22 | | xpss12 5604 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) → (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) |
23 | 21, 22 | impbid1 224 |
1
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |