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