Proof of Theorem ssxpb
| Step | Hyp | Ref
| Expression |
| 1 | | xpnz 6179 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) ↔ (𝐴 × 𝐵) ≠ ∅) |
| 2 | | dmxp 5939 |
. . . . . . . . 9
⊢ (𝐵 ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
| 3 | 2 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → dom (𝐴 × 𝐵) = 𝐴) |
| 4 | 1, 3 | sylbir 235 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → dom (𝐴 × 𝐵) = 𝐴) |
| 5 | 4 | adantr 480 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) = 𝐴) |
| 6 | | dmss 5913 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
| 7 | 6 | adantl 481 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → dom (𝐴 × 𝐵) ⊆ dom (𝐶 × 𝐷)) |
| 8 | 5, 7 | eqsstrrd 4019 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ dom (𝐶 × 𝐷)) |
| 9 | | dmxpss 6191 |
. . . . 5
⊢ dom
(𝐶 × 𝐷) ⊆ 𝐶 |
| 10 | 8, 9 | sstrdi 3996 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐴 ⊆ 𝐶) |
| 11 | | rnxp 6190 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
| 12 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅) → ran (𝐴 × 𝐵) = 𝐵) |
| 13 | 1, 12 | sylbir 235 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ≠ ∅ → ran (𝐴 × 𝐵) = 𝐵) |
| 14 | 13 | adantr 480 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) = 𝐵) |
| 15 | | rnss 5950 |
. . . . . . 7
⊢ ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
| 16 | 15 | adantl 481 |
. . . . . 6
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → ran (𝐴 × 𝐵) ⊆ ran (𝐶 × 𝐷)) |
| 17 | 14, 16 | eqsstrrd 4019 |
. . . . 5
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ ran (𝐶 × 𝐷)) |
| 18 | | rnxpss 6192 |
. . . . 5
⊢ ran
(𝐶 × 𝐷) ⊆ 𝐷 |
| 19 | 17, 18 | sstrdi 3996 |
. . . 4
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → 𝐵 ⊆ 𝐷) |
| 20 | 10, 19 | jca 511 |
. . 3
⊢ (((𝐴 × 𝐵) ≠ ∅ ∧ (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷)) |
| 21 | 20 | ex 412 |
. 2
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) → (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |
| 22 | | xpss12 5700 |
. 2
⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷) → (𝐴 × 𝐵) ⊆ (𝐶 × 𝐷)) |
| 23 | 21, 22 | impbid1 225 |
1
⊢ ((𝐴 × 𝐵) ≠ ∅ → ((𝐴 × 𝐵) ⊆ (𝐶 × 𝐷) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷))) |