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	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐶 ⊊ 𝐷 ) → ( 𝐴 × 𝐶 ) ⊊ ( 𝐵 × 𝐷 ) )