Step | Hyp | Ref
| Expression |
1 | | 1on 7454 |
. . . . . 6
⊢
1𝑜 ∈ On |
2 | 1 | elexi 3186 |
. . . . 5
⊢
1𝑜 ∈ V |
3 | | 1n0 7462 |
. . . . . 6
⊢
1𝑜 ≠ ∅ |
4 | | nelsn 4159 |
. . . . . 6
⊢
(1𝑜 ≠ ∅ → ¬ 1𝑜
∈ {∅}) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢ ¬
1𝑜 ∈ {∅} |
6 | | eldif 3550 |
. . . . . 6
⊢
(1𝑜 ∈ (V ∖ {∅}) ↔
(1𝑜 ∈ V ∧ ¬ 1𝑜 ∈
{∅})) |
7 | | ne0i 3880 |
. . . . . 6
⊢
(1𝑜 ∈ (V ∖ {∅}) → (V ∖
{∅}) ≠ ∅) |
8 | 6, 7 | sylbir 224 |
. . . . 5
⊢
((1𝑜 ∈ V ∧ ¬ 1𝑜
∈ {∅}) → (V ∖ {∅}) ≠ ∅) |
9 | 2, 5, 8 | mp2an 704 |
. . . 4
⊢ (V
∖ {∅}) ≠ ∅ |
10 | | r19.2zb 4013 |
. . . 4
⊢ ((V
∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)))) |
11 | 9, 10 | mpbi 219 |
. . 3
⊢
(∀𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
12 | | rexex 2985 |
. . 3
⊢
(∃𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
13 | | rexanali 2981 |
. . . . 5
⊢
(∃𝑘 ∈
(𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
14 | 13 | exbii 1764 |
. . . 4
⊢
(∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
15 | | exnal 1744 |
. . . 4
⊢
(∃𝑏 ¬
∀𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
16 | 14, 15 | sylbb 208 |
. . 3
⊢
(∃𝑏∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
17 | 11, 12, 16 | 3syl 18 |
. 2
⊢
(∀𝑏 ∈ (V
∖ {∅})∃𝑘
∈ (𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
18 | | id 22 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ∈ (V ∖
{∅})) |
19 | | difssd 3700 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑏 ∖ 𝑥) ⊆ 𝑏) |
20 | 18, 19 | sselpwd 4734 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏) |
21 | 20 | adantr 480 |
. . . . 5
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑥 ∈ 𝒫
𝑏) → (𝑏 ∖ 𝑥) ∈ 𝒫 𝑏) |
22 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) |
23 | 21, 22 | fmptd 6292 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏) |
24 | | pwexg 4776 |
. . . . 5
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝒫 𝑏 ∈
V) |
25 | 24, 24 | elmapd 7758 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ ((𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)):𝒫 𝑏⟶𝒫 𝑏)) |
26 | 23, 25 | mpbird 246 |
. . 3
⊢ (𝑏 ∈ (V ∖ {∅})
→ (𝑥 ∈ 𝒫
𝑏 ↦ (𝑏 ∖ 𝑥)) ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)) |
27 | | simpllr 795 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) |
28 | | difeq2 3684 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑏 ∖ 𝑥) = (𝑏 ∖ 𝑧)) |
29 | 28 | cbvmptv 4678 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧)) |
30 | 27, 29 | syl6eq 2660 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑧))) |
31 | | difeq2 3684 |
. . . . . . . . 9
⊢ (𝑧 = (𝑠 ∪ 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
32 | 31 | adantl 481 |
. . . . . . . 8
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠 ∪ 𝑡)) → (𝑏 ∖ 𝑧) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
33 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖
{∅})) |
34 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏) |
35 | 34 | elpwid 4118 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ⊆ 𝑏) |
36 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏) |
37 | 36 | elpwid 4118 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ⊆ 𝑏) |
38 | 35, 37 | unssd 3751 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ⊆ 𝑏) |
39 | 33, 38 | sselpwd 4734 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝑏) |
40 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
41 | 40 | difexi 4736 |
. . . . . . . . 9
⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V |
42 | 41 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ∈ V) |
43 | 30, 32, 39, 42 | fvmptd 6197 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠 ∪ 𝑡)) = (𝑏 ∖ (𝑠 ∪ 𝑡))) |
44 | | difeq2 3684 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠)) |
45 | 44 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑠)) |
46 | 40 | difexi 4736 |
. . . . . . . . . . 11
⊢ (𝑏 ∖ 𝑠) ∈ V |
47 | 46 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑠) ∈ V) |
48 | 30, 45, 34, 47 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑠) = (𝑏 ∖ 𝑠)) |
49 | | difeq2 3684 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑡 → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡)) |
50 | 49 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑏 ∈ (V
∖ {∅}) ∧ 𝑘
= (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏 ∖ 𝑧) = (𝑏 ∖ 𝑡)) |
51 | 40 | difexi 4736 |
. . . . . . . . . . 11
⊢ (𝑏 ∖ 𝑡) ∈ V |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ 𝑡) ∈ V) |
53 | 30, 50, 36, 52 | fvmptd 6197 |
. . . . . . . . 9
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘𝑡) = (𝑏 ∖ 𝑡)) |
54 | 48, 53 | uneq12d 3730 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡))) |
55 | | difindi 3840 |
. . . . . . . 8
⊢ (𝑏 ∖ (𝑠 ∩ 𝑡)) = ((𝑏 ∖ 𝑠) ∪ (𝑏 ∖ 𝑡)) |
56 | 54, 55 | syl6eqr 2662 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (𝑏 ∖ (𝑠 ∩ 𝑡))) |
57 | 43, 56 | sseq12d 3597 |
. . . . . 6
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
58 | 57 | ralbidva 2968 |
. . . . 5
⊢ (((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
59 | 58 | ralbidva 2968 |
. . . 4
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)))) |
60 | 56 | eqeq1d 2612 |
. . . . . . . 8
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
61 | 60 | imbi2d 329 |
. . . . . . 7
⊢ ((((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
62 | 61 | ralbidva 2968 |
. . . . . 6
⊢ (((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
63 | 62 | ralbidva 2968 |
. . . . 5
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
64 | 63 | notbid 307 |
. . . 4
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
65 | 59, 64 | anbi12d 743 |
. . 3
⊢ ((𝑏 ∈ (V ∖ {∅})
∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏 ∖ 𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)))) |
66 | | pwidg 4121 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ∈ 𝒫
𝑏) |
67 | | ssid 3587 |
. . . . . . 7
⊢ 𝑏 ⊆ 𝑏 |
68 | 67 | a1i 11 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ⊆ 𝑏) |
69 | | eldifsni 4261 |
. . . . . . 7
⊢ (𝑏 ∈ (V ∖ {∅})
→ 𝑏 ≠
∅) |
70 | 69 | neneqd 2787 |
. . . . . 6
⊢ (𝑏 ∈ (V ∖ {∅})
→ ¬ 𝑏 =
∅) |
71 | | uneq1 3722 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑏 → (𝑠 ∪ 𝑡) = (𝑏 ∪ 𝑡)) |
72 | 71 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏)) |
73 | | ssequn2 3748 |
. . . . . . . . 9
⊢ (𝑡 ⊆ 𝑏 ↔ (𝑏 ∪ 𝑡) = 𝑏) |
74 | 72, 73 | syl6bbr 277 |
. . . . . . . 8
⊢ (𝑠 = 𝑏 → ((𝑠 ∪ 𝑡) = 𝑏 ↔ 𝑡 ⊆ 𝑏)) |
75 | | ineq1 3769 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑏 → (𝑠 ∩ 𝑡) = (𝑏 ∩ 𝑡)) |
76 | 75 | difeq2d 3690 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = (𝑏 ∖ (𝑏 ∩ 𝑡))) |
77 | 76 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)) |
78 | 77 | notbid 307 |
. . . . . . . 8
⊢ (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏)) |
79 | 74, 78 | anbi12d 743 |
. . . . . . 7
⊢ (𝑠 = 𝑏 → (((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ (𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏))) |
80 | | sseq1 3589 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → (𝑡 ⊆ 𝑏 ↔ 𝑏 ⊆ 𝑏)) |
81 | | ineq2 3770 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = (𝑏 ∩ 𝑏)) |
82 | | inidm 3784 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∩ 𝑏) = 𝑏 |
83 | 81, 82 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (𝑡 = 𝑏 → (𝑏 ∩ 𝑡) = 𝑏) |
84 | 83 | difeq2d 3690 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = (𝑏 ∖ 𝑏)) |
85 | | difid 3902 |
. . . . . . . . . . . 12
⊢ (𝑏 ∖ 𝑏) = ∅ |
86 | 84, 85 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑏 → (𝑏 ∖ (𝑏 ∩ 𝑡)) = ∅) |
87 | 86 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ∅ = 𝑏)) |
88 | | eqcom 2617 |
. . . . . . . . . 10
⊢ (∅
= 𝑏 ↔ 𝑏 = ∅) |
89 | 87, 88 | syl6bb 275 |
. . . . . . . . 9
⊢ (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ 𝑏 = ∅)) |
90 | 89 | notbid 307 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅)) |
91 | 80, 90 | anbi12d 743 |
. . . . . . 7
⊢ (𝑡 = 𝑏 → ((𝑡 ⊆ 𝑏 ∧ ¬ (𝑏 ∖ (𝑏 ∩ 𝑡)) = 𝑏) ↔ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅))) |
92 | 79, 91 | rspc2ev 3295 |
. . . . . 6
⊢ ((𝑏 ∈ 𝒫 𝑏 ∧ 𝑏 ∈ 𝒫 𝑏 ∧ (𝑏 ⊆ 𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
93 | 66, 66, 68, 70, 92 | syl112anc 1322 |
. . . . 5
⊢ (𝑏 ∈ (V ∖ {∅})
→ ∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
94 | | rexanali 2981 |
. . . . . . 7
⊢
(∃𝑡 ∈
𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
95 | 94 | rexbii 3023 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
96 | | rexnal 2978 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 𝑏 ¬
∀𝑡 ∈ 𝒫
𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
97 | 95, 96 | sylbb 208 |
. . . . 5
⊢
(∃𝑠 ∈
𝒫 𝑏∃𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
98 | 93, 97 | syl 17 |
. . . 4
⊢ (𝑏 ∈ (V ∖ {∅})
→ ¬ ∀𝑠
∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏)) |
99 | | inss1 3795 |
. . . . . . 7
⊢ (𝑠 ∩ 𝑡) ⊆ 𝑠 |
100 | | ssun1 3738 |
. . . . . . 7
⊢ 𝑠 ⊆ (𝑠 ∪ 𝑡) |
101 | 99, 100 | sstri 3577 |
. . . . . 6
⊢ (𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) |
102 | | sscon 3706 |
. . . . . 6
⊢ ((𝑠 ∩ 𝑡) ⊆ (𝑠 ∪ 𝑡) → (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡))) |
103 | 101, 102 | ax-mp 5 |
. . . . 5
⊢ (𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) |
104 | 103 | rgen2w 2909 |
. . . 4
⊢
∀𝑠 ∈
𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) |
105 | 98, 104 | jctil 558 |
. . 3
⊢ (𝑏 ∈ (V ∖ {∅})
→ (∀𝑠 ∈
𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠 ∪ 𝑡)) ⊆ (𝑏 ∖ (𝑠 ∩ 𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → (𝑏 ∖ (𝑠 ∩ 𝑡)) = 𝑏))) |
106 | 26, 65, 105 | rspcedvd 3289 |
. 2
⊢ (𝑏 ∈ (V ∖ {∅})
→ ∃𝑘 ∈
(𝒫 𝑏
↑𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏))) |
107 | 17, 106 | mprg 2910 |
1
⊢ ¬
∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏((𝑠 ∪ 𝑡) = 𝑏 → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = 𝑏)) |