Proof of Theorem disjord
Step | Hyp | Ref
| Expression |
1 | | orc 864 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
2 | 1 | a1d 25 |
. . . . 5
⊢ (𝑎 = 𝑏 → (𝜑 → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅))) |
3 | | disjord.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑎 = 𝑏) |
4 | 3 | 3expia 1118 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 → 𝑎 = 𝑏)) |
5 | 4 | con3d 155 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (¬ 𝑎 = 𝑏 → ¬ 𝑥 ∈ 𝐵)) |
6 | 5 | impancom 455 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑏) → (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)) |
7 | 6 | ralrimiv 3148 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑏) → ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
8 | | disj 4355 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵) |
9 | 7, 8 | sylibr 237 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑏) → (𝐴 ∩ 𝐵) = ∅) |
10 | 9 | olcd 871 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑏) → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
11 | 10 | expcom 417 |
. . . . 5
⊢ (¬
𝑎 = 𝑏 → (𝜑 → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅))) |
12 | 2, 11 | pm2.61i 185 |
. . . 4
⊢ (𝜑 → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
13 | 12 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
14 | 13 | ralrimivva 3156 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
15 | | disjord.1 |
. . 3
⊢ (𝑎 = 𝑏 → 𝐴 = 𝐵) |
16 | 15 | disjor 5010 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 𝐴 ↔ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑎 = 𝑏 ∨ (𝐴 ∩ 𝐵) = ∅)) |
17 | 14, 16 | sylibr 237 |
1
⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 𝐴) |