Step | Hyp | Ref
| Expression |
1 | | eleq1 2233 |
. 2
⊢ (𝑤 = ∅ → (𝑤 ∈ Omni ↔ ∅
∈ Omni)) |
2 | | eleq1 2233 |
. 2
⊢ (𝑤 = 𝑦 → (𝑤 ∈ Omni ↔ 𝑦 ∈ Omni)) |
3 | | eleq1 2233 |
. 2
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 ∈ Omni ↔ (𝑦 ∪ {𝑧}) ∈ Omni)) |
4 | | eleq1 2233 |
. 2
⊢ (𝑤 = 𝐴 → (𝑤 ∈ Omni ↔ 𝐴 ∈ Omni)) |
5 | | 0ex 4114 |
. . . 4
⊢ ∅
∈ V |
6 | | isomni 7108 |
. . . 4
⊢ (∅
∈ V → (∅ ∈ Omni ↔ ∀𝑓(𝑓:∅⟶2o →
(∃𝑥 ∈ ∅
(𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ ∅ (𝑓‘𝑥) = 1o)))) |
7 | 5, 6 | ax-mp 5 |
. . 3
⊢ (∅
∈ Omni ↔ ∀𝑓(𝑓:∅⟶2o →
(∃𝑥 ∈ ∅
(𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ ∅ (𝑓‘𝑥) = 1o))) |
8 | | ral0 3515 |
. . . . 5
⊢
∀𝑥 ∈
∅ (𝑓‘𝑥) =
1o |
9 | 8 | olci 727 |
. . . 4
⊢
(∃𝑥 ∈
∅ (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ ∅ (𝑓‘𝑥) = 1o) |
10 | 9 | a1i 9 |
. . 3
⊢ (𝑓:∅⟶2o
→ (∃𝑥 ∈
∅ (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ ∅ (𝑓‘𝑥) = 1o)) |
11 | 7, 10 | mpgbir 1446 |
. 2
⊢ ∅
∈ Omni |
12 | | elun1 3294 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑦 → 𝑥 ∈ (𝑦 ∪ {𝑧})) |
13 | 12 | ad2antlr 486 |
. . . . . . . . . . 11
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → 𝑥 ∈ (𝑦 ∪ {𝑧})) |
14 | | fvres 5518 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑦 → ((𝑔 ↾ 𝑦)‘𝑥) = (𝑔‘𝑥)) |
15 | 14 | ad2antlr 486 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → ((𝑔 ↾ 𝑦)‘𝑥) = (𝑔‘𝑥)) |
16 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → ((𝑔 ↾ 𝑦)‘𝑥) = ∅) |
17 | 15, 16 | eqtr3d 2205 |
. . . . . . . . . . 11
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → (𝑔‘𝑥) = ∅) |
18 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑥 → (𝑔‘𝑢) = (𝑔‘𝑥)) |
19 | 18 | eqeq1d 2179 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑥 → ((𝑔‘𝑢) = ∅ ↔ (𝑔‘𝑥) = ∅)) |
20 | 19 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝑦 ∪ {𝑧}) ∧ (𝑔‘𝑥) = ∅) → ∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅) |
21 | 13, 17, 20 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → ∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅) |
22 | 21 | orcd 728 |
. . . . . . . . 9
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) ∧ ((𝑔 ↾ 𝑦)‘𝑥) = ∅) → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o)) |
23 | 22 | ex 114 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ 𝑥 ∈ 𝑦) → (((𝑔 ↾ 𝑦)‘𝑥) = ∅ → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
24 | 23 | rexlimdva 2587 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
25 | | vsnid 3613 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ {𝑧} |
26 | | elun2 3295 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ {𝑧} → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
27 | 25, 26 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ (𝑦 ∪ {𝑧}) |
28 | 27 | a1i 9 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → 𝑧 ∈ (𝑦 ∪ {𝑧})) |
29 | | fveq2 5494 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → (𝑔‘𝑢) = (𝑔‘𝑧)) |
30 | 29 | eqeq1d 2179 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑧 → ((𝑔‘𝑢) = ∅ ↔ (𝑔‘𝑧) = ∅)) |
31 | 30 | rspcev 2834 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ (𝑦 ∪ {𝑧}) ∧ (𝑔‘𝑧) = ∅) → ∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅) |
32 | 28, 31 | sylan 281 |
. . . . . . . . . 10
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = ∅) → ∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅) |
33 | 32 | orcd 728 |
. . . . . . . . 9
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = ∅) → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o)) |
34 | 33 | a1d 22 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = ∅) → (∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
35 | | simpr 109 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) |
36 | | fveq2 5494 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑢 → ((𝑔 ↾ 𝑦)‘𝑥) = ((𝑔 ↾ 𝑦)‘𝑢)) |
37 | 36 | eqeq1d 2179 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑢 → (((𝑔 ↾ 𝑦)‘𝑥) = 1o ↔ ((𝑔 ↾ 𝑦)‘𝑢) = 1o)) |
38 | 37 | cbvralv 2696 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o ↔ ∀𝑢 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑢) = 1o) |
39 | | fvres 5518 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ 𝑦 → ((𝑔 ↾ 𝑦)‘𝑢) = (𝑔‘𝑢)) |
40 | 39 | eqeq1d 2179 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈ 𝑦 → (((𝑔 ↾ 𝑦)‘𝑢) = 1o ↔ (𝑔‘𝑢) = 1o)) |
41 | 40 | ralbiia 2484 |
. . . . . . . . . . . . 13
⊢
(∀𝑢 ∈
𝑦 ((𝑔 ↾ 𝑦)‘𝑢) = 1o ↔ ∀𝑢 ∈ 𝑦 (𝑔‘𝑢) = 1o) |
42 | 38, 41 | bitri 183 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o ↔ ∀𝑢 ∈ 𝑦 (𝑔‘𝑢) = 1o) |
43 | 35, 42 | sylib 121 |
. . . . . . . . . . 11
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → ∀𝑢 ∈ 𝑦 (𝑔‘𝑢) = 1o) |
44 | | simplr 525 |
. . . . . . . . . . . 12
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → (𝑔‘𝑧) = 1o) |
45 | | vex 2733 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
46 | 29 | eqeq1d 2179 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑧 → ((𝑔‘𝑢) = 1o ↔ (𝑔‘𝑧) = 1o)) |
47 | 45, 46 | ralsn 3624 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
{𝑧} (𝑔‘𝑢) = 1o ↔ (𝑔‘𝑧) = 1o) |
48 | 44, 47 | sylibr 133 |
. . . . . . . . . . 11
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → ∀𝑢 ∈ {𝑧} (𝑔‘𝑢) = 1o) |
49 | | ralun 3309 |
. . . . . . . . . . 11
⊢
((∀𝑢 ∈
𝑦 (𝑔‘𝑢) = 1o ∧ ∀𝑢 ∈ {𝑧} (𝑔‘𝑢) = 1o) → ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o) |
50 | 43, 48, 49 | syl2anc 409 |
. . . . . . . . . 10
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o) |
51 | 50 | olcd 729 |
. . . . . . . . 9
⊢
(((((𝑦 ∈ Fin
∧ 𝑦 ∈ Omni) ∧
𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) ∧ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o) → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o)) |
52 | 51 | ex 114 |
. . . . . . . 8
⊢ ((((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) ∧ (𝑔‘𝑧) = 1o) → (∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
53 | | simpr 109 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → 𝑔:(𝑦 ∪ {𝑧})⟶2o) |
54 | 53, 28 | ffvelrnd 5629 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → (𝑔‘𝑧) ∈ 2o) |
55 | | df2o3 6406 |
. . . . . . . . . 10
⊢
2o = {∅, 1o} |
56 | 54, 55 | eleqtrdi 2263 |
. . . . . . . . 9
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → (𝑔‘𝑧) ∈ {∅,
1o}) |
57 | | elpri 3604 |
. . . . . . . . 9
⊢ ((𝑔‘𝑧) ∈ {∅, 1o} →
((𝑔‘𝑧) = ∅ ∨ (𝑔‘𝑧) = 1o)) |
58 | 56, 57 | syl 14 |
. . . . . . . 8
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → ((𝑔‘𝑧) = ∅ ∨ (𝑔‘𝑧) = 1o)) |
59 | 34, 52, 58 | mpjaodan 793 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) →
(∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
60 | | vex 2733 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
61 | | isomni 7108 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ V → (𝑦 ∈ Omni ↔
∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Omni ↔
∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))) |
63 | 62 | biimpi 119 |
. . . . . . . . . 10
⊢ (𝑦 ∈ Omni →
∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))) |
64 | 63 | adantl 275 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) →
∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o))) |
65 | | vex 2733 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
66 | 65 | resex 4930 |
. . . . . . . . . 10
⊢ (𝑔 ↾ 𝑦) ∈ V |
67 | | feq1 5328 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ 𝑦) → (𝑓:𝑦⟶2o ↔ (𝑔 ↾ 𝑦):𝑦⟶2o)) |
68 | | fveq1 5493 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑔 ↾ 𝑦) → (𝑓‘𝑥) = ((𝑔 ↾ 𝑦)‘𝑥)) |
69 | 68 | eqeq1d 2179 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ↾ 𝑦) → ((𝑓‘𝑥) = ∅ ↔ ((𝑔 ↾ 𝑦)‘𝑥) = ∅)) |
70 | 69 | rexbidv 2471 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ↾ 𝑦) → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ↔ ∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅)) |
71 | 68 | eqeq1d 2179 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ↾ 𝑦) → ((𝑓‘𝑥) = 1o ↔ ((𝑔 ↾ 𝑦)‘𝑥) = 1o)) |
72 | 71 | ralbidv 2470 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ↾ 𝑦) → (∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o ↔ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o)) |
73 | 70, 72 | orbi12d 788 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ↾ 𝑦) → ((∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o) ↔ (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o))) |
74 | 67, 73 | imbi12d 233 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ↾ 𝑦) → ((𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)) ↔ ((𝑔 ↾ 𝑦):𝑦⟶2o → (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o)))) |
75 | 66, 74 | spcv 2824 |
. . . . . . . . 9
⊢
(∀𝑓(𝑓:𝑦⟶2o → (∃𝑥 ∈ 𝑦 (𝑓‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 (𝑓‘𝑥) = 1o)) → ((𝑔 ↾ 𝑦):𝑦⟶2o → (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o))) |
76 | 64, 75 | syl 14 |
. . . . . . . 8
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) → ((𝑔 ↾ 𝑦):𝑦⟶2o → (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o))) |
77 | | ssun1 3290 |
. . . . . . . . 9
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
78 | | fssres 5371 |
. . . . . . . . 9
⊢ ((𝑔:(𝑦 ∪ {𝑧})⟶2o ∧ 𝑦 ⊆ (𝑦 ∪ {𝑧})) → (𝑔 ↾ 𝑦):𝑦⟶2o) |
79 | 77, 78 | mpan2 423 |
. . . . . . . 8
⊢ (𝑔:(𝑦 ∪ {𝑧})⟶2o → (𝑔 ↾ 𝑦):𝑦⟶2o) |
80 | 76, 79 | impel 278 |
. . . . . . 7
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → (∃𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = ∅ ∨ ∀𝑥 ∈ 𝑦 ((𝑔 ↾ 𝑦)‘𝑥) = 1o)) |
81 | 24, 59, 80 | mpjaod 713 |
. . . . . 6
⊢ (((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) ∧ 𝑔:(𝑦 ∪ {𝑧})⟶2o) → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o)) |
82 | 81 | ex 114 |
. . . . 5
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) → (𝑔:(𝑦 ∪ {𝑧})⟶2o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
83 | 82 | alrimiv 1867 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) →
∀𝑔(𝑔:(𝑦 ∪ {𝑧})⟶2o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
84 | 45 | snex 4169 |
. . . . . 6
⊢ {𝑧} ∈ V |
85 | 60, 84 | unex 4424 |
. . . . 5
⊢ (𝑦 ∪ {𝑧}) ∈ V |
86 | | isomni 7108 |
. . . . 5
⊢ ((𝑦 ∪ {𝑧}) ∈ V → ((𝑦 ∪ {𝑧}) ∈ Omni ↔ ∀𝑔(𝑔:(𝑦 ∪ {𝑧})⟶2o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o)))) |
87 | 85, 86 | ax-mp 5 |
. . . 4
⊢ ((𝑦 ∪ {𝑧}) ∈ Omni ↔ ∀𝑔(𝑔:(𝑦 ∪ {𝑧})⟶2o → (∃𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = ∅ ∨ ∀𝑢 ∈ (𝑦 ∪ {𝑧})(𝑔‘𝑢) = 1o))) |
88 | 83, 87 | sylibr 133 |
. . 3
⊢ ((𝑦 ∈ Fin ∧ 𝑦 ∈ Omni) → (𝑦 ∪ {𝑧}) ∈ Omni) |
89 | 88 | ex 114 |
. 2
⊢ (𝑦 ∈ Fin → (𝑦 ∈ Omni → (𝑦 ∪ {𝑧}) ∈ Omni)) |
90 | 1, 2, 3, 4, 11, 89 | findcard2 6863 |
1
⊢ (𝐴 ∈ Fin → 𝐴 ∈ Omni) |