Metamath Proof Explorer


Theorem disjxp1

Description: The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis disjxp1.1 ( 𝜑Disj 𝑥𝐴 𝐵 )
Assertion disjxp1 ( 𝜑Disj 𝑥𝐴 ( 𝐵 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 disjxp1.1 ( 𝜑Disj 𝑥𝐴 𝐵 )
2 animorrl ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦 = 𝑧 ) → ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ ) )
3 csbxp 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) = ( 𝑦 / 𝑥 𝐵 × 𝑦 / 𝑥 𝐶 )
4 csbxp 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) = ( 𝑧 / 𝑥 𝐵 × 𝑧 / 𝑥 𝐶 )
5 3 4 ineq12i ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ( ( 𝑦 / 𝑥 𝐵 × 𝑦 / 𝑥 𝐶 ) ∩ ( 𝑧 / 𝑥 𝐵 × 𝑧 / 𝑥 𝐶 ) )
6 simpll ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → 𝜑 )
7 simplrl ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → 𝑦𝐴 )
8 simplrr ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → 𝑧𝐴 )
9 6 7 8 jca31 ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ( ( 𝜑𝑦𝐴 ) ∧ 𝑧𝐴 ) )
10 simpr ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → 𝑦𝑧 )
11 10 neneqd ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ¬ 𝑦 = 𝑧 )
12 disjors ( Disj 𝑥𝐴 𝐵 ↔ ∀ 𝑦𝐴𝑧𝐴 ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ ) )
13 1 12 sylib ( 𝜑 → ∀ 𝑦𝐴𝑧𝐴 ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ ) )
14 13 r19.21bi ( ( 𝜑𝑦𝐴 ) → ∀ 𝑧𝐴 ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ ) )
15 14 r19.21bi ( ( ( 𝜑𝑦𝐴 ) ∧ 𝑧𝐴 ) → ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ ) )
16 15 ord ( ( ( 𝜑𝑦𝐴 ) ∧ 𝑧𝐴 ) → ( ¬ 𝑦 = 𝑧 → ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ ) )
17 9 11 16 sylc ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ )
18 xpdisj1 ( ( 𝑦 / 𝑥 𝐵 𝑧 / 𝑥 𝐵 ) = ∅ → ( ( 𝑦 / 𝑥 𝐵 × 𝑦 / 𝑥 𝐶 ) ∩ ( 𝑧 / 𝑥 𝐵 × 𝑧 / 𝑥 𝐶 ) ) = ∅ )
19 17 18 syl ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ( ( 𝑦 / 𝑥 𝐵 × 𝑦 / 𝑥 𝐶 ) ∩ ( 𝑧 / 𝑥 𝐵 × 𝑧 / 𝑥 𝐶 ) ) = ∅ )
20 5 19 syl5eq ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ )
21 20 olcd ( ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) ∧ 𝑦𝑧 ) → ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ ) )
22 2 21 pm2.61dane ( ( 𝜑 ∧ ( 𝑦𝐴𝑧𝐴 ) ) → ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ ) )
23 22 ralrimivva ( 𝜑 → ∀ 𝑦𝐴𝑧𝐴 ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ ) )
24 disjors ( Disj 𝑥𝐴 ( 𝐵 × 𝐶 ) ↔ ∀ 𝑦𝐴𝑧𝐴 ( 𝑦 = 𝑧 ∨ ( 𝑦 / 𝑥 ( 𝐵 × 𝐶 ) ∩ 𝑧 / 𝑥 ( 𝐵 × 𝐶 ) ) = ∅ ) )
25 23 24 sylibr ( 𝜑Disj 𝑥𝐴 ( 𝐵 × 𝐶 ) )