Proof of Theorem ssxpb
Step | Hyp | Ref
| Expression |
1 | | xpnz 5991 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) |
2 | | dmxp 5772 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
3 | 2 | adantl 485 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → dom (𝐴 × 𝐵) = 𝐴) |
4 | 1, 3 | sylbir 238 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) = 𝐴) |
6 | | dmss 5745 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
7 | 6 | adantl 485 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
8 | 5, 7 | eqsstrrd 3916 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ dom (𝐶 × 𝐷)) |
9 | | dmxpss 6003 |
. . . . 5
⊢ dom
(𝐶 × 𝐷) ⊆ 𝐶 |
10 | 8, 9 | sstrdi 3889 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ 𝐶) |
11 | | rnxp 6002 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ran (𝐴 × 𝐵) = 𝐵) |
13 | 1, 12 | sylbir 238 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
14 | 13 | adantr 484 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) = 𝐵) |
15 | | rnss 5782 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
16 | 15 | adantl 485 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
17 | 14, 16 | eqsstrrd 3916 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ ran (𝐶 × 𝐷)) |
18 | | rnxpss 6004 |
. . . . 5
⊢ ran
(𝐶 × 𝐷) ⊆ 𝐷 |
19 | 17, 18 | sstrdi 3889 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ 𝐷) |
20 | 10, 19 | jca 515 |
. . 3
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)) |
21 | 20 | ex 416 |
. 2
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
22 | | xpss12 5540 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) → (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) |
23 | 21, 22 | impbid1 228 |
1
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |