Step | Hyp | Ref
| Expression |
1 | | exmidomniim 7117 |
. 2
⊢
(EXMID → ∀𝑥 𝑥 ∈ Omni) |
2 | | vex 2733 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
3 | | eleq1w 2231 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → (𝑥 ∈ Omni ↔ 𝑢 ∈ Omni)) |
4 | 2, 3 | spcv 2824 |
. . . . . . . . 9
⊢
(∀𝑥 𝑥 ∈ Omni → 𝑢 ∈ Omni) |
5 | | xpeq1 4625 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (𝑥 × {∅}) = (𝑢 × {∅})) |
6 | 5 | fveq1d 5498 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑢 → ((𝑥 × {∅})‘𝑦) = ((𝑢 × {∅})‘𝑦)) |
7 | 6 | eqeq1d 2179 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (((𝑥 × {∅})‘𝑦) = ∅ ↔ ((𝑢 × {∅})‘𝑦) = ∅)) |
8 | 7 | rexeqbi1dv 2674 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ↔ ∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅)) |
9 | 6 | eqeq1d 2179 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑢 → (((𝑥 × {∅})‘𝑦) = 1o ↔ ((𝑢 × {∅})‘𝑦) = 1o)) |
10 | 9 | raleqbi1dv 2673 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑢 → (∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o ↔ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o)) |
11 | 8, 10 | orbi12d 788 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → ((∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o) ↔ (∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o))) |
12 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
13 | | isomni 7112 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ V → (𝑥 ∈ Omni ↔
∀𝑓(𝑓:𝑥⟶2o → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o)))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ Omni ↔
∀𝑓(𝑓:𝑥⟶2o → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o))) |
15 | 14 | biimpi 119 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Omni →
∀𝑓(𝑓:𝑥⟶2o → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o))) |
16 | | 0ex 4116 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ V |
17 | 16 | prid1 3689 |
. . . . . . . . . . . . 13
⊢ ∅
∈ {∅, 1o} |
18 | | df2o3 6409 |
. . . . . . . . . . . . 13
⊢
2o = {∅, 1o} |
19 | 17, 18 | eleqtrri 2246 |
. . . . . . . . . . . 12
⊢ ∅
∈ 2o |
20 | 19 | fconst6 5397 |
. . . . . . . . . . 11
⊢ (𝑥 × {∅}):𝑥⟶2o |
21 | | p0ex 4174 |
. . . . . . . . . . . . 13
⊢ {∅}
∈ V |
22 | 12, 21 | xpex 4726 |
. . . . . . . . . . . 12
⊢ (𝑥 × {∅}) ∈
V |
23 | | feq1 5330 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑥 × {∅}) → (𝑓:𝑥⟶2o ↔ (𝑥 × {∅}):𝑥⟶2o)) |
24 | | fveq1 5495 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑥 × {∅}) → (𝑓‘𝑦) = ((𝑥 × {∅})‘𝑦)) |
25 | 24 | eqeq1d 2179 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑥 × {∅}) → ((𝑓‘𝑦) = ∅ ↔ ((𝑥 × {∅})‘𝑦) = ∅)) |
26 | 25 | rexbidv 2471 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 × {∅}) → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ↔ ∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅)) |
27 | 24 | eqeq1d 2179 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑥 × {∅}) → ((𝑓‘𝑦) = 1o ↔ ((𝑥 × {∅})‘𝑦) = 1o)) |
28 | 27 | ralbidv 2470 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑥 × {∅}) → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o ↔ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o)) |
29 | 26, 28 | orbi12d 788 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑥 × {∅}) → ((∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o) ↔ (∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o))) |
30 | 23, 29 | imbi12d 233 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑥 × {∅}) → ((𝑓:𝑥⟶2o → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o)) ↔ ((𝑥 × {∅}):𝑥⟶2o →
(∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o)))) |
31 | 22, 30 | spcv 2824 |
. . . . . . . . . . 11
⊢
(∀𝑓(𝑓:𝑥⟶2o → (∃𝑦 ∈ 𝑥 (𝑓‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = 1o)) → ((𝑥 × {∅}):𝑥⟶2o →
(∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o))) |
32 | 15, 20, 31 | mpisyl 1439 |
. . . . . . . . . 10
⊢ (𝑥 ∈ Omni →
(∃𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑥 ((𝑥 × {∅})‘𝑦) = 1o)) |
33 | 11, 32 | vtoclga 2796 |
. . . . . . . . 9
⊢ (𝑢 ∈ Omni →
(∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o)) |
34 | 4, 33 | syl 14 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 ∈ Omni →
(∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o)) |
35 | 34 | adantr 274 |
. . . . . . 7
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
(∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o)) |
36 | | simplr 525 |
. . . . . . . . . 10
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅) → 𝑢 ⊆ {∅}) |
37 | | rexm 3514 |
. . . . . . . . . . . 12
⊢
(∃𝑦 ∈
𝑢 ((𝑢 × {∅})‘𝑦) = ∅ → ∃𝑦 𝑦 ∈ 𝑢) |
38 | | sssnm 3741 |
. . . . . . . . . . . 12
⊢
(∃𝑦 𝑦 ∈ 𝑢 → (𝑢 ⊆ {∅} ↔ 𝑢 = {∅})) |
39 | 37, 38 | syl 14 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
𝑢 ((𝑢 × {∅})‘𝑦) = ∅ → (𝑢 ⊆ {∅} ↔ 𝑢 = {∅})) |
40 | 39 | adantl 275 |
. . . . . . . . . 10
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅) → (𝑢 ⊆ {∅} ↔ 𝑢 = {∅})) |
41 | 36, 40 | mpbid 146 |
. . . . . . . . 9
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅) → 𝑢 = {∅}) |
42 | 41 | ex 114 |
. . . . . . . 8
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
(∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ → 𝑢 = {∅})) |
43 | | nfv 1521 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦(∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) |
44 | | nfra1 2501 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑦∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o |
45 | 43, 44 | nfan 1558 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) |
46 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦𝑢 |
47 | | nfcv 2312 |
. . . . . . . . . . 11
⊢
Ⅎ𝑦∅ |
48 | | 1n0 6411 |
. . . . . . . . . . . . . 14
⊢
1o ≠ ∅ |
49 | 48 | neii 2342 |
. . . . . . . . . . . . 13
⊢ ¬
1o = ∅ |
50 | | simpr 109 |
. . . . . . . . . . . . . . . 16
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) |
51 | 50 | r19.21bi 2558 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) ∧ 𝑦 ∈ 𝑢) → ((𝑢 × {∅})‘𝑦) = 1o) |
52 | 16 | fvconst2 5712 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝑢 → ((𝑢 × {∅})‘𝑦) = ∅) |
53 | 52 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢
((((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) ∧ 𝑦 ∈ 𝑢) → ((𝑢 × {∅})‘𝑦) = ∅) |
54 | 51, 53 | eqtr3d 2205 |
. . . . . . . . . . . . . 14
⊢
((((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) ∧ 𝑦 ∈ 𝑢) → 1o =
∅) |
55 | 54 | ex 114 |
. . . . . . . . . . . . 13
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → (𝑦 ∈ 𝑢 → 1o =
∅)) |
56 | 49, 55 | mtoi 659 |
. . . . . . . . . . . 12
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → ¬ 𝑦 ∈ 𝑢) |
57 | 56 | pm2.21d 614 |
. . . . . . . . . . 11
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → (𝑦 ∈ 𝑢 → 𝑦 ∈ ∅)) |
58 | 45, 46, 47, 57 | ssrd 3152 |
. . . . . . . . . 10
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → 𝑢 ⊆ ∅) |
59 | | ss0 3455 |
. . . . . . . . . 10
⊢ (𝑢 ⊆ ∅ → 𝑢 = ∅) |
60 | 58, 59 | syl 14 |
. . . . . . . . 9
⊢
(((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) ∧
∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → 𝑢 = ∅) |
61 | 60 | ex 114 |
. . . . . . . 8
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
(∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o → 𝑢 = ∅)) |
62 | 42, 61 | orim12d 781 |
. . . . . . 7
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
((∃𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = ∅ ∨ ∀𝑦 ∈ 𝑢 ((𝑢 × {∅})‘𝑦) = 1o) → (𝑢 = {∅} ∨ 𝑢 = ∅))) |
63 | 35, 62 | mpd 13 |
. . . . . 6
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
(𝑢 = {∅} ∨ 𝑢 = ∅)) |
64 | 63 | orcomd 724 |
. . . . 5
⊢
((∀𝑥 𝑥 ∈ Omni ∧ 𝑢 ⊆ {∅}) →
(𝑢 = ∅ ∨ 𝑢 = {∅})) |
65 | 64 | ex 114 |
. . . 4
⊢
(∀𝑥 𝑥 ∈ Omni → (𝑢 ⊆ {∅} → (𝑢 = ∅ ∨ 𝑢 = {∅}))) |
66 | 65 | alrimiv 1867 |
. . 3
⊢
(∀𝑥 𝑥 ∈ Omni →
∀𝑢(𝑢 ⊆ {∅} → (𝑢 = ∅ ∨ 𝑢 = {∅}))) |
67 | | exmid01 4184 |
. . 3
⊢
(EXMID ↔ ∀𝑢(𝑢 ⊆ {∅} → (𝑢 = ∅ ∨ 𝑢 = {∅}))) |
68 | 66, 67 | sylibr 133 |
. 2
⊢
(∀𝑥 𝑥 ∈ Omni →
EXMID) |
69 | 1, 68 | impbii 125 |
1
⊢
(EXMID ↔ ∀𝑥 𝑥 ∈ Omni) |