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 𝑥 ∈ 𝐴 ( 𝐵 × 𝐶 ) ) |