Step | Hyp | Ref
| Expression |
1 | | df-ne 2936 |
. . 3
⊢ (𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌) |
2 | | disjors 5012 |
. . . . . 6
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
3 | | eqeq1 2743 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → (𝑦 = 𝑧 ↔ 𝑋 = 𝑧)) |
4 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑋 |
5 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐶 |
6 | | disji.1 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶) |
7 | 4, 5, 6 | csbhypf 3819 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑋 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐶) |
8 | 7 | ineq1d 4103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑋 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
9 | 8 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑦 = 𝑋 → ((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
10 | 3, 9 | orbi12d 918 |
. . . . . . 7
⊢ (𝑦 = 𝑋 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 = 𝑧 ∨ (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅))) |
11 | | eqeq2 2751 |
. . . . . . . 8
⊢ (𝑧 = 𝑌 → (𝑋 = 𝑧 ↔ 𝑋 = 𝑌)) |
12 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑌 |
13 | | nfcv 2900 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐷 |
14 | | disji.2 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑌 → 𝐵 = 𝐷) |
15 | 12, 13, 14 | csbhypf 3819 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐷) |
16 | 15 | ineq2d 4104 |
. . . . . . . . 9
⊢ (𝑧 = 𝑌 → (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐶 ∩ 𝐷)) |
17 | 16 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑧 = 𝑌 → ((𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐶 ∩ 𝐷) = ∅)) |
18 | 11, 17 | orbi12d 918 |
. . . . . . 7
⊢ (𝑧 = 𝑌 → ((𝑋 = 𝑧 ∨ (𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑋 = 𝑌 ∨ (𝐶 ∩ 𝐷) = ∅))) |
19 | 10, 18 | rspc2v 3537 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑋 = 𝑌 ∨ (𝐶 ∩ 𝐷) = ∅))) |
20 | 2, 19 | syl5bi 245 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (Disj 𝑥 ∈ 𝐴 𝐵 → (𝑋 = 𝑌 ∨ (𝐶 ∩ 𝐷) = ∅))) |
21 | 20 | impcom 411 |
. . . 4
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 = 𝑌 ∨ (𝐶 ∩ 𝐷) = ∅)) |
22 | 21 | ord 863 |
. . 3
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (¬ 𝑋 = 𝑌 → (𝐶 ∩ 𝐷) = ∅)) |
23 | 1, 22 | syl5bi 245 |
. 2
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋 ≠ 𝑌 → (𝐶 ∩ 𝐷) = ∅)) |
24 | 23 | 3impia 1118 |
1
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ 𝑋 ≠ 𝑌) → (𝐶 ∩ 𝐷) = ∅) |