Step | Hyp | Ref
| Expression |
1 | | elex 2720 |
. 2
⊢ (𝐴 ∈ Omni → 𝐴 ∈ V) |
2 | | simpl 108 |
. . 3
⊢ ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ WOmni) |
3 | 2 | elexd 2722 |
. 2
⊢ ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) → 𝐴 ∈ V) |
4 | | 1n0 6369 |
. . . . . . . . . . . . . . 15
⊢
1o ≠ ∅ |
5 | 4 | nesymi 2370 |
. . . . . . . . . . . . . 14
⊢ ¬
∅ = 1o |
6 | | eqeq1 2161 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) = 1o ↔ ∅ =
1o)) |
7 | 5, 6 | mtbiri 665 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑥) = ∅ → ¬ (𝑓‘𝑥) = 1o) |
8 | 7 | reximi 2551 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 (𝑓‘𝑥) = ∅ → ∃𝑥 ∈ 𝐴 ¬ (𝑓‘𝑥) = 1o) |
9 | | rexnalim 2443 |
. . . . . . . . . . . 12
⊢
(∃𝑥 ∈
𝐴 ¬ (𝑓‘𝑥) = 1o → ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) |
10 | 8, 9 | syl 14 |
. . . . . . . . . . 11
⊢
(∃𝑥 ∈
𝐴 (𝑓‘𝑥) = ∅ → ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) |
11 | 10 | orim1i 750 |
. . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
12 | 11 | orcomd 719 |
. . . . . . . . 9
⊢
((∃𝑥 ∈
𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
13 | | df-dc 821 |
. . . . . . . . 9
⊢
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ↔ (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
14 | 12, 13 | sylibr 133 |
. . . . . . . 8
⊢
((∃𝑥 ∈
𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) |
15 | 14 | adantl 275 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) |
16 | | simpr 109 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
17 | 16 | orcomd 719 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
18 | 17 | ord 714 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
19 | 15, 18 | jca 304 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧ (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) |
20 | | simprl 521 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → DECID
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) |
21 | 20, 13 | sylib 121 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
22 | | simprr 522 |
. . . . . . . . 9
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
23 | 22 | orim2d 778 |
. . . . . . . 8
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → ((∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) |
24 | 21, 23 | mpd 13 |
. . . . . . 7
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∨ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)) |
25 | 24 | orcomd 719 |
. . . . . 6
⊢ (((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) ∧
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) |
26 | 19, 25 | impbida 586 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝑓:𝐴⟶2o) → ((∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ↔
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) |
27 | 26 | pm5.74da 440 |
. . . 4
⊢ (𝐴 ∈ V → ((𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) ↔ (𝑓:𝐴⟶2o →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))) |
28 | 27 | albidv 1801 |
. . 3
⊢ (𝐴 ∈ V → (∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)) ↔ ∀𝑓(𝑓:𝐴⟶2o →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))) |
29 | | isomni 7058 |
. . 3
⊢ (𝐴 ∈ V → (𝐴 ∈ Omni ↔
∀𝑓(𝑓:𝐴⟶2o → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o)))) |
30 | | iswomni 7087 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ∈ WOmni ↔
∀𝑓(𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o))) |
31 | | ismkv 7075 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝐴 ∈ Markov ↔
∀𝑓(𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) |
32 | 30, 31 | anbi12d 465 |
. . . . 5
⊢ (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔
(∀𝑓(𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))) |
33 | | 19.26 1458 |
. . . . 5
⊢
(∀𝑓((𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) ↔ (∀𝑓(𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ ∀𝑓(𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) |
34 | 32, 33 | bitr4di 197 |
. . . 4
⊢ (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔
∀𝑓((𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))) |
35 | | jcab 593 |
. . . . 5
⊢ ((𝑓:𝐴⟶2o →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) ↔ ((𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) |
36 | 35 | albii 1447 |
. . . 4
⊢
(∀𝑓(𝑓:𝐴⟶2o →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))) ↔ ∀𝑓((𝑓:𝐴⟶2o →
DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o) ∧ (𝑓:𝐴⟶2o → (¬
∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅)))) |
37 | 34, 36 | bitr4di 197 |
. . 3
⊢ (𝐴 ∈ V → ((𝐴 ∈ WOmni ∧ 𝐴 ∈ Markov) ↔
∀𝑓(𝑓:𝐴⟶2o →
(DECID ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o ∧ (¬ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) = 1o → ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = ∅))))) |
38 | 28, 29, 37 | 3bitr4d 219 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈
Markov))) |
39 | 1, 3, 38 | pm5.21nii 694 |
1
⊢ (𝐴 ∈ Omni ↔ (𝐴 ∈ WOmni ∧ 𝐴 ∈
Markov)) |