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 eqtrid ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ) = ∅ )
21 20 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑦 ≠ 𝑧 ) → ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ) = ∅ ) )
22 2 21 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ) = ∅ ) )
23 22 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ) = ∅ ) )
24 disjors ⊢ ( Disj 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 = 𝑧 ∨ ( ⦋ 𝑦 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ∩ ⦋ 𝑧 / 𝑥 ⦌ ( 𝐵 × 𝐶 ) ) = ∅ ) )
25 23 24 sylibr ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) )