Step | Hyp | Ref
| Expression |
1 | | inelcm 4398 |
. 2
⊢ ((𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (𝐵 ∩ 𝐶) ≠ ∅) |
2 | | disjif2.1 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐴 |
3 | 2 | disjorsf 30919 |
. . . . . . 7
⊢
(Disj 𝑥
∈ 𝐴 𝐵 ↔ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
4 | | equequ1 2028 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 = 𝑧 ↔ 𝑥 = 𝑧)) |
5 | | csbeq1 3835 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵) |
6 | | csbid 3845 |
. . . . . . . . . . . 12
⊢
⦋𝑥 /
𝑥⦌𝐵 = 𝐵 |
7 | 5, 6 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → ⦋𝑦 / 𝑥⦌𝐵 = 𝐵) |
8 | 7 | ineq1d 4145 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵)) |
9 | 8 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → ((⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅)) |
10 | 4, 9 | orbi12d 916 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑥 = 𝑧 ∨ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅))) |
11 | | eqeq2 2750 |
. . . . . . . . 9
⊢ (𝑧 = 𝑌 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑌)) |
12 | | nfcv 2907 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑌 |
13 | | disjif2.2 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐶 |
14 | | disjif2.3 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑌 → 𝐵 = 𝐶) |
15 | 12, 13, 14 | csbhypf 3861 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑌 → ⦋𝑧 / 𝑥⦌𝐵 = 𝐶) |
16 | 15 | ineq2d 4146 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑌 → (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = (𝐵 ∩ 𝐶)) |
17 | 16 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑧 = 𝑌 → ((𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅ ↔ (𝐵 ∩ 𝐶) = ∅)) |
18 | 11, 17 | orbi12d 916 |
. . . . . . . 8
⊢ (𝑧 = 𝑌 → ((𝑥 = 𝑧 ∨ (𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) ↔ (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
19 | 10, 18 | rspc2v 3570 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐵 ∩ ⦋𝑧 / 𝑥⦌𝐵) = ∅) → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
20 | 3, 19 | syl5bi 241 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (Disj 𝑥 ∈ 𝐴 𝐵 → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅))) |
21 | 20 | impcom 408 |
. . . . 5
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑥 = 𝑌 ∨ (𝐵 ∩ 𝐶) = ∅)) |
22 | 21 | ord 861 |
. . . 4
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (¬ 𝑥 = 𝑌 → (𝐵 ∩ 𝐶) = ∅)) |
23 | 22 | necon1ad 2960 |
. . 3
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → ((𝐵 ∩ 𝐶) ≠ ∅ → 𝑥 = 𝑌)) |
24 | 23 | 3impia 1116 |
. 2
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝐵 ∩ 𝐶) ≠ ∅) → 𝑥 = 𝑌) |
25 | 1, 24 | syl3an3 1164 |
1
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) ∧ (𝑍 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝑥 = 𝑌) |