Proof of Theorem exmidontriimlem1
Step | Hyp | Ref
| Expression |
1 | | 3orass 966 |
. . . . . . . 8
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
2 | 1 | biimpi 119 |
. . . . . . 7
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒))) |
3 | 2 | orcomd 719 |
. . . . . 6
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) → ((𝜓 ∨ 𝜒) ∨ 𝜑)) |
4 | 3 | ralimi 2520 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) → ∀𝑥 ∈ 𝐴 ((𝜓 ∨ 𝜒) ∨ 𝜑)) |
5 | | exmidexmid 4157 |
. . . . 5
⊢
(EXMID → DECID ∃𝑥 ∈ 𝐴 𝜑) |
6 | | r19.30dc 2604 |
. . . . 5
⊢
((∀𝑥 ∈
𝐴 ((𝜓 ∨ 𝜒) ∨ 𝜑) ∧ DECID ∃𝑥 ∈ 𝐴 𝜑) → (∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒) ∨ ∃𝑥 ∈ 𝐴 𝜑)) |
7 | 4, 5, 6 | syl2an 287 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
(∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒) ∨ ∃𝑥 ∈ 𝐴 𝜑)) |
8 | 7 | orcomd 719 |
. . 3
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
(∃𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒))) |
9 | | simpr 109 |
. . . . . 6
⊢
(((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) ∧
∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒)) → ∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒)) |
10 | | simplr 520 |
. . . . . 6
⊢
(((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) ∧
∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒)) →
EXMID) |
11 | | orcom 718 |
. . . . . . . . . 10
⊢ ((𝜓 ∨ 𝜒) ↔ (𝜒 ∨ 𝜓)) |
12 | 11 | ralbii 2463 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 (𝜓 ∨ 𝜒) ↔ ∀𝑥 ∈ 𝐴 (𝜒 ∨ 𝜓)) |
13 | 12 | biimpi 119 |
. . . . . . . 8
⊢
(∀𝑥 ∈
𝐴 (𝜓 ∨ 𝜒) → ∀𝑥 ∈ 𝐴 (𝜒 ∨ 𝜓)) |
14 | | exmidexmid 4157 |
. . . . . . . 8
⊢
(EXMID → DECID ∃𝑥 ∈ 𝐴 𝜓) |
15 | | r19.30dc 2604 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐴 (𝜒 ∨ 𝜓) ∧ DECID ∃𝑥 ∈ 𝐴 𝜓) → (∀𝑥 ∈ 𝐴 𝜒 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
16 | 13, 14, 15 | syl2an 287 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐴 (𝜓 ∨ 𝜒) ∧ EXMID) →
(∀𝑥 ∈ 𝐴 𝜒 ∨ ∃𝑥 ∈ 𝐴 𝜓)) |
17 | 16 | orcomd 719 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐴 (𝜓 ∨ 𝜒) ∧ EXMID) →
(∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒)) |
18 | 9, 10, 17 | syl2anc 409 |
. . . . 5
⊢
(((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) ∧
∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒)) → (∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒)) |
19 | 18 | ex 114 |
. . . 4
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
(∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒) → (∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))) |
20 | 19 | orim2d 778 |
. . 3
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
((∃𝑥 ∈ 𝐴 𝜑 ∨ ∀𝑥 ∈ 𝐴 (𝜓 ∨ 𝜒)) → (∃𝑥 ∈ 𝐴 𝜑 ∨ (∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒)))) |
21 | 8, 20 | mpd 13 |
. 2
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
(∃𝑥 ∈ 𝐴 𝜑 ∨ (∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))) |
22 | | 3orass 966 |
. 2
⊢
((∃𝑥 ∈
𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∨ (∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒))) |
23 | 21, 22 | sylibr 133 |
1
⊢
((∀𝑥 ∈
𝐴 (𝜑 ∨ 𝜓 ∨ 𝜒) ∧ EXMID) →
(∃𝑥 ∈ 𝐴 𝜑 ∨ ∃𝑥 ∈ 𝐴 𝜓 ∨ ∀𝑥 ∈ 𝐴 𝜒)) |