Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . 3
⊢ (𝑥 ≠ 𝑌 ↔ ¬ 𝑥 = 𝑌) |
2 | | disjors 5034 |
. . . . . 6
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
3 | | equequ1 2033 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑥 = 𝑧)) |
4 | | csbeq1 3814 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵) |
5 | | csbid 3824 |
. . . . . . . . . . 11
⊢
⦋𝑥 /
𝑥⦌𝐵 = 𝐵 |
6 | 4, 5 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐵) |
7 | 6 | ineq1d 4126 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
8 | 7 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
9 | 3, 8 | orbi12d 919 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑥 = 𝑧 ∨ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅))) |
10 | | eqeq2 2749 |
. . . . . . . 8
⊢ (𝑧 = 𝑌 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑌)) |
11 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑌 |
12 | | disjif.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐶 |
13 | | disjif.2 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) |
14 | 11, 12, 13 | csbhypf 3840 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐶) |
15 | 14 | ineq2d 4127 |
. . . . . . . . 9
⊢ (𝑧 = 𝑌 → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ 𝐶)) |
16 | 15 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑧 = 𝑌 → ((𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐵 ∩ 𝐶) = ∅)) |
17 | 10, 16 | orbi12d 919 |
. . . . . . 7
⊢ (𝑧 = 𝑌 → ((𝑥 = 𝑧 ∨ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
18 | 9, 17 | rspc2v 3547 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
19 | 2, 18 | syl5bi 245 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (Disj 𝑥 ∈ 𝐴 𝐵 → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
20 | 19 | impcom 411 |
. . . 4
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅)) |
21 | 20 | ord 864 |
. . 3
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (¬ 𝑥 = 𝑌 → (𝐵 ∩ 𝐶) = ∅)) |
22 | 1, 21 | syl5bi 245 |
. 2
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑥 ≠ 𝑌 → (𝐵 ∩ 𝐶) = ∅)) |
23 | 22 | 3impia 1119 |
1
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑥 ≠ 𝑌) → (𝐵 ∩ 𝐶) = ∅) |