Step | Hyp | Ref
| Expression |
1 | | 1oex 7738 |
. . . . 5
⊢
1𝑜 ∈ V |
2 | | 1n0 7746 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
3 | | nelsn 4357 |
. . . . . 6
⊢
(1𝑜 ≠ ∅ → ¬ 1𝑜
∈ {∅}) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ ¬
1𝑜 ∈ {∅} |
5 | | eldif 3725 |
. . . . . 6
⊢
(1𝑜 ∈ (V ∖ {∅}) ↔
(1𝑜 ∈ V ∧ ¬ 1𝑜 ∈
{∅})) |
6 | | ne0i 4064 |
. . . . . 6
⊢
(1𝑜 ∈ (V ∖ {∅}) → (V ∖
{∅}) ≠ ∅) |
7 | 5, 6 | sylbir 225 |
. . . . 5
⊢
((1𝑜 ∈ V ∧ ¬ 1𝑜
∈ {∅}) → (V ∖ {∅}) ≠ ∅) |
8 | 1, 4, 7 | mp2an 710 |
. . . 4
⊢ (V
∖ {∅}) ≠ ∅ |
9 | | r19.2zb 4205 |
. . . 4
⊢ ((V
∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))) |
10 | 8, 9 | mpbi 220 |
. . 3
⊢
(∀𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
11 | | rexex 3140 |
. . 3
⊢
(∃𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
12 | | rexanali 3136 |
. . . . 5
⊢
(∃𝑘 ∈
(𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
13 | 12 | exbii 1923 |
. . . 4
⊢
(∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
14 | | exnal 1903 |
. . . 4
⊢
(∃𝑏 ¬
∀𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
15 | 13, 14 | sylbb 209 |
. . 3
⊢
(∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
16 | 10, 11, 15 | 3syl 18 |
. 2
⊢
(∀𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
17 | | id 22 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ∈ (V ∖
{∅})) |
18 | | difssd 3881 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑏 ∖ 𝑥) ⊆ 𝑏) |
19 | 17, 18 | sselpwd 4959 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏) |
20 | 19 | adantr 472 |
. . . . 5
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑥 ∈ 𝒫
𝑏) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏) |
21 | | eqid 2760 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) |
22 | 20, 21 | fmptd 6549 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏) |
23 | | pwexg 4999 |
. . . . 5
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝒫 𝑏 ∈
V) |
24 | 23, 23 | elmapd 8039 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ ((𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏)) |
25 | 22, 24 | mpbird 247 |
. . 3
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)) |
26 | | simpllr 817 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) |
27 | | difeq2 3865 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑏 ∖ 𝑥) = (𝑏 ∖ 𝑧)) |
28 | 27 | cbvmptv 4902 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧)) |
29 | 26, 28 | syl6eq 2810 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧))) |
30 | | difeq2 3865 |
. . . . . . . . 9
⊢ (𝑧 = (𝑠 ∪ 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
31 | 30 | adantl 473 |
. . . . . . . 8
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 ∪ 𝑡)) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
32 | | simplll 815 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖
{∅})) |
33 | | simplr 809 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏) |
34 | 33 | elpwid 4314 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ⊆ 𝑏) |
35 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏) |
36 | 35 | elpwid 4314 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ⊆ 𝑏) |
37 | 34, 36 | unssd 3932 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ⊆ 𝑏) |
38 | 32, 37 | sselpwd 4959 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝑏) |
39 | | vex 3343 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
40 | 39 | difexi 4961 |
. . . . . . . . 9
⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V |
41 | 40 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V) |
42 | 29, 31, 38, 41 | fvmptd 6451 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠 ∪ 𝑡)) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
43 | | difeq2 3865 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠)) |
44 | 43 | adantl 473 |
. . . . . . . . . 10
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠)) |
45 | 39 | difexi 4961 |
. . . . . . . . . . 11
⊢ (𝑏 ∖ 𝑠) ∈ V |
46 | 45 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑠) ∈ V) |
47 | 29, 44, 33, 46 | fvmptd 6451 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑠) = (𝑏 ∖ 𝑠)) |
48 | | difeq2 3865 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡)) |
49 | 48 | adantl 473 |
. . . . . . . . . 10
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡)) |
50 | 39 | difexi 4961 |
. . . . . . . . . . 11
⊢ (𝑏 ∖ 𝑡) ∈ V |
51 | 50 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑡) ∈ V) |
52 | 29, 49, 35, 51 | fvmptd 6451 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑡) = (𝑏 ∖ 𝑡)) |
53 | 47, 52 | uneq12d 3911 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡))) |
54 | | difindi 4024 |
. . . . . . . 8
⊢ (𝑏 ∖ (𝑠 ∩ 𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡)) |
55 | 53, 54 | syl6eqr 2812 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (𝑏 ∖ (𝑠 ∩ 𝑡))) |
56 | 42, 55 | sseq12d 3775 |
. . . . . 6
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
57 | 56 | ralbidva 3123 |
. . . . 5
⊢ (((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
58 | 57 | ralbidva 3123 |
. . . 4
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
59 | 55 | eqeq1d 2762 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
60 | 59 | imbi2d 329 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
61 | 60 | ralbidva 3123 |
. . . . . 6
⊢ (((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
62 | 61 | ralbidva 3123 |
. . . . 5
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
63 | 62 | notbid 307 |
. . . 4
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
64 | 58, 63 | anbi12d 749 |
. . 3
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))) |
65 | | pwidg 4317 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ∈ 𝒫
𝑏) |
66 | | ssid 3765 |
. . . . . . 7
⊢ 𝑏 ⊆ 𝑏 |
67 | 66 | a1i 11 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ⊆ 𝑏) |
68 | | eldifsni 4466 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ≠
∅) |
69 | 68 | neneqd 2937 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ ¬ 𝑏 =
∅) |
70 | | uneq1 3903 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑏 → (𝑠 ∪ 𝑡) = (𝑏 ∪ 𝑡)) |
71 | 70 | eqeq1d 2762 |
. . . . . . . . 9
⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏)) |
72 | | ssequn2 3929 |
. . . . . . . . 9
⊢ (𝑡 ⊆ 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏) |
73 | 71, 72 | syl6bbr 278 |
. . . . . . . 8
⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ 𝑡 ⊆ 𝑏)) |
74 | | ineq1 3950 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑏 → (𝑠 ∩ 𝑡) = (𝑏 ∩ 𝑡)) |
75 | 74 | difeq2d 3871 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = (𝑏 ∖ (𝑏 ∩ 𝑡))) |
76 | 75 | eqeq1d 2762 |
. . . . . . . . 9
⊢ (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)) |
77 | 76 | notbid 307 |
. . . . . . . 8
⊢ (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)) |
78 | 73, 77 | anbi12d 749 |
. . . . . . 7
⊢ (𝑠 = 𝑏 → (((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ (𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))) |
79 | | sseq1 3767 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → (𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏)) |
80 | | ineq2 3951 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = (𝑏 ∩ 𝑏)) |
81 | | inidm 3965 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∩ 𝑏) = 𝑏 |
82 | 80, 81 | syl6eq 2810 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = 𝑏) |
83 | 82 | difeq2d 3871 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = (𝑏 ∖ 𝑏)) |
84 | | difid 4091 |
. . . . . . . . . . . 12
⊢ (𝑏 ∖ 𝑏) = ∅ |
85 | 83, 84 | syl6eq 2810 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = ∅) |
86 | 85 | eqeq1d 2762 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ∅ = 𝑏)) |
87 | | eqcom 2767 |
. . . . . . . . . 10
⊢ (∅
= 𝑏 ↔ 𝑏 = ∅) |
88 | 86, 87 | syl6bb 276 |
. . . . . . . . 9
⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ 𝑏 = ∅)) |
89 | 88 | notbid 307 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅)) |
90 | 79, 89 | anbi12d 749 |
. . . . . . 7
⊢ (𝑡 = 𝑏 → ((𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏) ↔ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅))) |
91 | 78, 90 | rspc2ev 3463 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
92 | 65, 65, 67, 69, 91 | syl112anc 1481 |
. . . . 5
⊢ (𝑏 ∈ (V ∖ {∅})
→ ∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
93 | | rexanali 3136 |
. . . . . . 7
⊢
(∃𝑡 ∈
𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
94 | 93 | rexbii 3179 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
95 | | rexnal 3133 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 𝑏 ¬
∀𝑡 ∈ 𝒫
𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
96 | 94, 95 | sylbb 209 |
. . . . 5
⊢
(∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
97 | 92, 96 | syl 17 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ ¬ ∀𝑠
∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
98 | | inss1 3976 |
. . . . . . 7
⊢ (𝑠 ∩ 𝑡) ⊆ 𝑠 |
99 | | ssun1 3919 |
. . . . . . 7
⊢ 𝑠 ⊆ (𝑠 ∪ 𝑡) |
100 | 98, 99 | sstri 3753 |
. . . . . 6
⊢ (𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) |
101 | | sscon 3887 |
. . . . . 6
⊢ ((𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))) |
102 | 100, 101 | ax-mp 5 |
. . . . 5
⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) |
103 | 102 | rgen2w 3063 |
. . . 4
⊢
∀𝑠 ∈
𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) |
104 | 97, 103 | jctil 561 |
. . 3
⊢ (𝑏 ∈ (V ∖ {∅})
→ (∀𝑠 ∈
𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
105 | 25, 64, 104 | rspcedvd 3456 |
. 2
⊢ (𝑏 ∈ (V ∖ {∅})
→ ∃𝑘 ∈
(𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
106 | 16, 105 | mprg 3064 |
1
⊢ ¬
∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) |