This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xppss12

Description: Proper subset theorem for Cartesian product. (Contributed by Steven Nguyen, 17-Jul-2022)

Ref Expression
Assertion xppss12 ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( 𝐴 × 𝐶 ) ⊊ ( 𝐵 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 pssss ⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 )
2 pssss ⊢ ( 𝐶 ⊊ 𝐷 → 𝐶 ⊆ 𝐷 )
3 xpss12 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( 𝐴 × 𝐶 ) ⊆ ( 𝐵 × 𝐷 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( 𝐴 × 𝐶 ) ⊆ ( 𝐵 × 𝐷 ) )
5 simpl ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → 𝐴 ⊊ 𝐵 )
6 pssne ⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ≠ 𝐵 )
7 6 necomd ⊢ ( 𝐴 ⊊ 𝐵 → 𝐵 ≠ 𝐴 )
8 neneq ⊢ ( 𝐵 ≠ 𝐴 → ¬ 𝐵 = 𝐴 )
9 8 intnanrd ⊢ ( 𝐵 ≠ 𝐴 → ¬ ( 𝐵 = 𝐴 ∧ 𝐷 = 𝐶 ) )
10 5 7 9 3syl ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ¬ ( 𝐵 = 𝐴 ∧ 𝐷 = 𝐶 ) )
11 pssn0 ⊢ ( 𝐴 ⊊ 𝐵 → 𝐵 ≠ ∅ )
12 pssn0 ⊢ ( 𝐶 ⊊ 𝐷 → 𝐷 ≠ ∅ )
13 xp11 ⊢ ( ( 𝐵 ≠ ∅ ∧ 𝐷 ≠ ∅ ) → ( ( 𝐵 × 𝐷 ) = ( 𝐴 × 𝐶 ) ↔ ( 𝐵 = 𝐴 ∧ 𝐷 = 𝐶 ) ) )
14 11 12 13 syl2an ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( ( 𝐵 × 𝐷 ) = ( 𝐴 × 𝐶 ) ↔ ( 𝐵 = 𝐴 ∧ 𝐷 = 𝐶 ) ) )
15 10 14 mtbird ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ¬ ( 𝐵 × 𝐷 ) = ( 𝐴 × 𝐶 ) )
16 neqne ⊢ ( ¬ ( 𝐵 × 𝐷 ) = ( 𝐴 × 𝐶 ) → ( 𝐵 × 𝐷 ) ≠ ( 𝐴 × 𝐶 ) )
17 16 necomd ⊢ ( ¬ ( 𝐵 × 𝐷 ) = ( 𝐴 × 𝐶 ) → ( 𝐴 × 𝐶 ) ≠ ( 𝐵 × 𝐷 ) )
18 15 17 syl ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( 𝐴 × 𝐶 ) ≠ ( 𝐵 × 𝐷 ) )
19 df-pss ⊢ ( ( 𝐴 × 𝐶 ) ⊊ ( 𝐵 × 𝐷 ) ↔ ( ( 𝐴 × 𝐶 ) ⊆ ( 𝐵 × 𝐷 ) ∧ ( 𝐴 × 𝐶 ) ≠ ( 𝐵 × 𝐷 ) ) )
20 4 18 19 sylanbrc ⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( 𝐴 × 𝐶 ) ⊊ ( 𝐵 × 𝐷 ) )