Proof of Theorem disjiund
Step | Hyp | Ref
| Expression |
1 | | eliun 4928 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 ↔ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) |
2 | | eliun 4928 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑏 ∈ 𝑋 𝐶 ↔ ∃𝑏 ∈ 𝑋 𝑥 ∈ 𝐶) |
3 | | disjiund.2 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑑 → 𝐶 = 𝐷) |
4 | 3 | eleq2d 2824 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑑 → (𝑥 ∈ 𝐶 ↔ 𝑥 ∈ 𝐷)) |
5 | 4 | cbvrexvw 3384 |
. . . . . . . . . . . . 13
⊢
(∃𝑏 ∈
𝑋 𝑥 ∈ 𝐶 ↔ ∃𝑑 ∈ 𝑋 𝑥 ∈ 𝐷) |
6 | | disjiund.4 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐷) → 𝑎 = 𝑐) |
7 | 6 | 3exp 1118 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐷 → 𝑎 = 𝑐))) |
8 | 7 | rexlimdvw 3219 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐷 → 𝑎 = 𝑐))) |
9 | 8 | imp 407 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐷 → 𝑎 = 𝑐)) |
10 | 9 | rexlimdvw 3219 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) → (∃𝑑 ∈ 𝑋 𝑥 ∈ 𝐷 → 𝑎 = 𝑐)) |
11 | 5, 10 | syl5bi 241 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝑋 𝑥 ∈ 𝐶 → 𝑎 = 𝑐)) |
12 | 2, 11 | syl5bi 241 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) → (𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶 → 𝑎 = 𝑐)) |
13 | 12 | con3d 152 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴) → (¬ 𝑎 = 𝑐 → ¬ 𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶)) |
14 | 13 | impancom 452 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑐) → (∃𝑏 ∈ 𝑊 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶)) |
15 | 1, 14 | syl5bi 241 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑐) → (𝑥 ∈ ∪
𝑏 ∈ 𝑊 𝐴 → ¬ 𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶)) |
16 | 15 | ralrimiv 3102 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑐) → ∀𝑥 ∈ ∪
𝑏 ∈ 𝑊 𝐴 ¬ 𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶) |
17 | | disj 4381 |
. . . . . . 7
⊢
((∪ 𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅ ↔ ∀𝑥 ∈ ∪ 𝑏 ∈ 𝑊 𝐴 ¬ 𝑥 ∈ ∪
𝑏 ∈ 𝑋 𝐶) |
18 | 16, 17 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑎 = 𝑐) → (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅) |
19 | 18 | ex 413 |
. . . . 5
⊢ (𝜑 → (¬ 𝑎 = 𝑐 → (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅)) |
20 | 19 | orrd 860 |
. . . 4
⊢ (𝜑 → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅)) |
21 | 20 | a1d 25 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉) → (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅))) |
22 | 21 | ralrimivv 3122 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅)) |
23 | | disjiund.3 |
. . 3
⊢ (𝑎 = 𝑐 → 𝑊 = 𝑋) |
24 | | disjiund.1 |
. . 3
⊢ (𝑎 = 𝑐 → 𝐴 = 𝐶) |
25 | 23, 24 | disjiunb 5063 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴 ↔ ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ 𝑉 (𝑎 = 𝑐 ∨ (∪
𝑏 ∈ 𝑊 𝐴 ∩ ∪
𝑏 ∈ 𝑋 𝐶) = ∅)) |
26 | 22, 25 | sylibr 233 |
1
⊢ (𝜑 → Disj 𝑎 ∈ 𝑉 ∪ 𝑏 ∈ 𝑊 𝐴) |