Metamath Proof Explorer

Theorem ssxpb

Description: A Cartesian product subclass relationship is equivalent to the conjunction of the analogous relationships for the factors. (Contributed by NM, 17-Dec-2008)

Ref Expression
Assertion ssxpb ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 xpnz ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) ↔ ( 𝐴 × 𝐵 ) ≠ ∅ )
2 dmxp ⊢ ( 𝐵 ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
3 2 adantl ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → dom ( 𝐴 × 𝐵 ) = 𝐴 )
4 1 3 sylbir ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → dom ( 𝐴 × 𝐵 ) = 𝐴 )
5 4 adantr ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → dom ( 𝐴 × 𝐵 ) = 𝐴 )
6 dmss ⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) → dom ( 𝐴 × 𝐵 ) ⊆ dom ( 𝐶 × 𝐷 ) )
7 6 adantl ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → dom ( 𝐴 × 𝐵 ) ⊆ dom ( 𝐶 × 𝐷 ) )
8 5 7 eqsstrrd ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → 𝐴 ⊆ dom ( 𝐶 × 𝐷 ) )
9 dmxpss ⊢ dom ( 𝐶 × 𝐷 ) ⊆ 𝐶
10 8 9 sstrdi ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → 𝐴 ⊆ 𝐶 )
11 rnxp ⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
12 11 adantr ⊢ ( ( 𝐴 ≠ ∅ ∧ 𝐵 ≠ ∅ ) → ran ( 𝐴 × 𝐵 ) = 𝐵 )
13 1 12 sylbir ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
14 13 adantr ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → ran ( 𝐴 × 𝐵 ) = 𝐵 )
15 rnss ⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) → ran ( 𝐴 × 𝐵 ) ⊆ ran ( 𝐶 × 𝐷 ) )
16 15 adantl ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → ran ( 𝐴 × 𝐵 ) ⊆ ran ( 𝐶 × 𝐷 ) )
17 14 16 eqsstrrd ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → 𝐵 ⊆ ran ( 𝐶 × 𝐷 ) )
18 rnxpss ⊢ ran ( 𝐶 × 𝐷 ) ⊆ 𝐷
19 17 18 sstrdi ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → 𝐵 ⊆ 𝐷 )
20 10 19 jca ⊢ ( ( ( 𝐴 × 𝐵 ) ≠ ∅ ∧ ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) )
21 20 ex ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) → ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ) )
22 xpss12 ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) )
23 21 22 impbid1 ⊢ ( ( 𝐴 × 𝐵 ) ≠ ∅ → ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐶 × 𝐷 ) ↔ ( 𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐷 ) ) )