Step | Hyp | Ref
| Expression |
1 | | exmidexmid 4031 |
. . . . . . . . 9
⊢
(EXMID → DECID ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜) |
2 | | exmiddc 782 |
. . . . . . . . 9
⊢
(DECID ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 →
(∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 ∨ ¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
3 | 1, 2 | syl 14 |
. . . . . . . 8
⊢
(EXMID → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 ∨ ¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
4 | 3 | orcomd 683 |
. . . . . . 7
⊢
(EXMID → (¬ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
5 | 4 | adantr 270 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) → (¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
6 | | ffvelrn 5432 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝑥⟶2𝑜 ∧ 𝑦 ∈ 𝑥) → (𝑓‘𝑦) ∈
2𝑜) |
7 | | df2o3 6195 |
. . . . . . . . . . . . . 14
⊢
2𝑜 = {∅,
1𝑜} |
8 | 6, 7 | syl6eleq 2180 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑥⟶2𝑜 ∧ 𝑦 ∈ 𝑥) → (𝑓‘𝑦) ∈ {∅,
1𝑜}) |
9 | | elpri 3469 |
. . . . . . . . . . . . 13
⊢ ((𝑓‘𝑦) ∈ {∅, 1𝑜}
→ ((𝑓‘𝑦) = ∅ ∨ (𝑓‘𝑦) = 1𝑜)) |
10 | 8, 9 | syl 14 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝑥⟶2𝑜 ∧ 𝑦 ∈ 𝑥) → ((𝑓‘𝑦) = ∅ ∨ (𝑓‘𝑦) = 1𝑜)) |
11 | 10 | ord 678 |
. . . . . . . . . . 11
⊢ ((𝑓:𝑥⟶2𝑜 ∧ 𝑦 ∈ 𝑥) → (¬ (𝑓‘𝑦) = ∅ → (𝑓‘𝑦) = 1𝑜)) |
12 | 11 | ralimdva 2441 |
. . . . . . . . . 10
⊢ (𝑓:𝑥⟶2𝑜 →
(∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅ → ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
13 | 12 | con3d 596 |
. . . . . . . . 9
⊢ (𝑓:𝑥⟶2𝑜 → (¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 → ¬
∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅)) |
14 | 13 | adantl 271 |
. . . . . . . 8
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) → (¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 → ¬
∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅)) |
15 | | exmidexmid 4031 |
. . . . . . . . . 10
⊢
(EXMID → DECID ∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅) |
16 | | dfrex2dc 2371 |
. . . . . . . . . 10
⊢
(DECID ∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ↔ ¬ ∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅)) |
17 | 15, 16 | syl 14 |
. . . . . . . . 9
⊢
(EXMID → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ↔ ¬ ∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅)) |
18 | 17 | adantr 270 |
. . . . . . . 8
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ↔ ¬ ∀𝑦 ∈ 𝑥 ¬ (𝑓‘𝑦) = ∅)) |
19 | 14, 18 | sylibrd 167 |
. . . . . . 7
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) → (¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 → ∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅)) |
20 | 19 | orim1d 736 |
. . . . . 6
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) → ((¬
∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜 ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜) →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜))) |
21 | 5, 20 | mpd 13 |
. . . . 5
⊢
((EXMID ∧ 𝑓:𝑥⟶2𝑜) →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜)) |
22 | 21 | ex 113 |
. . . 4
⊢
(EXMID → (𝑓:𝑥⟶2𝑜 →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜))) |
23 | 22 | alrimiv 1802 |
. . 3
⊢
(EXMID → ∀𝑓(𝑓:𝑥⟶2𝑜 →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜))) |
24 | | vex 2622 |
. . . 4
⊢ 𝑥 ∈ V |
25 | | isomni 6790 |
. . . 4
⊢ (𝑥 ∈ V → (𝑥 ∈ Omni ↔
∀𝑓(𝑓:𝑥⟶2𝑜 →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) =
1𝑜)))) |
26 | 24, 25 | ax-mp 7 |
. . 3
⊢ (𝑥 ∈ Omni ↔
∀𝑓(𝑓:𝑥⟶2𝑜 →
(∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1𝑜))) |
27 | 23, 26 | sylibr 132 |
. 2
⊢
(EXMID → 𝑥 ∈ Omni) |
28 | 27 | alrimiv 1802 |
1
⊢
(EXMID → ∀𝑥 𝑥 ∈ Omni) |