Step | Hyp | Ref
| Expression |
1 | | orc 894 |
. . . . 5
⊢ (𝑦 = 𝑧 → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
2 | 1 | adantl 474 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 = 𝑧) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
3 | | simpl 475 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑧) → (𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
4 | | neqne 2979 |
. . . . . 6
⊢ (¬
𝑦 = 𝑧 → 𝑦 ≠ 𝑧) |
5 | 4 | adantl 474 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑧) → 𝑦 ≠ 𝑧) |
6 | | csbxp 5405 |
. . . . . . . . 9
⊢
⦋𝑦 /
𝑥⦌(𝐵 × 𝐶) = (⦋𝑦 / 𝑥⦌𝐵 × ⦋𝑦 / 𝑥⦌𝐶) |
7 | | csbxp 5405 |
. . . . . . . . 9
⊢
⦋𝑧 /
𝑥⦌(𝐵 × 𝐶) = (⦋𝑧 / 𝑥⦌𝐵 × ⦋𝑧 / 𝑥⦌𝐶) |
8 | 6, 7 | ineq12i 4010 |
. . . . . . . 8
⊢
(⦋𝑦 /
𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ((⦋𝑦 / 𝑥⦌𝐵 × ⦋𝑦 / 𝑥⦌𝐶) ∩ (⦋𝑧 / 𝑥⦌𝐵 × ⦋𝑧 / 𝑥⦌𝐶)) |
9 | 8 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ((⦋𝑦 / 𝑥⦌𝐵 × ⦋𝑦 / 𝑥⦌𝐶) ∩ (⦋𝑧 / 𝑥⦌𝐵 × ⦋𝑧 / 𝑥⦌𝐶))) |
10 | | simpll 784 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → 𝜑) |
11 | | simplrl 796 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ 𝐴) |
12 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ 𝐴) |
13 | 10, 11, 12 | jca31 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → ((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴)) |
14 | | simpr 478 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
15 | 14 | neneqd 2976 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → ¬ 𝑦 = 𝑧) |
16 | | disjxp1.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
17 | | disjors 4826 |
. . . . . . . . . . . . 13
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
18 | 16, 17 | sylib 210 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
19 | 18 | r19.21bi 3113 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
20 | 19 | r19.21bi 3113 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
21 | 20 | ord 891 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (¬ 𝑦 = 𝑧 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
22 | 13, 15, 21 | sylc 65 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) |
23 | | xpdisj1 5772 |
. . . . . . . 8
⊢
((⦋𝑦 /
𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ → ((⦋𝑦 / 𝑥⦌𝐵 × ⦋𝑦 / 𝑥⦌𝐶) ∩ (⦋𝑧 / 𝑥⦌𝐵 × ⦋𝑧 / 𝑥⦌𝐶)) = ∅) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → ((⦋𝑦 / 𝑥⦌𝐵 × ⦋𝑦 / 𝑥⦌𝐶) ∩ (⦋𝑧 / 𝑥⦌𝐵 × ⦋𝑧 / 𝑥⦌𝐶)) = ∅) |
25 | 9, 24 | eqtrd 2833 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅) |
26 | | olc 895 |
. . . . . 6
⊢
((⦋𝑦 /
𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅ → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
27 | 25, 26 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ 𝑦 ≠ 𝑧) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
28 | 3, 5, 27 | syl2anc 580 |
. . . 4
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ¬ 𝑦 = 𝑧) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
29 | 2, 28 | pm2.61dan 848 |
. . 3
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
30 | 29 | ralrimivva 3152 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
31 | | disjors 4826 |
. 2
⊢
(Disj 𝑥
∈ 𝐴 (𝐵 × 𝐶) ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌(𝐵 × 𝐶) ∩ ⦋𝑧 / 𝑥⦌(𝐵 × 𝐶)) = ∅)) |
32 | 30, 31 | sylibr 226 |
1
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 (𝐵 × 𝐶)) |