Users' Mathboxes Mathbox for Richard Penner < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  clsk3nimkb Structured version   Visualization version   GIF version

Theorem clsk3nimkb 41327
Description: If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) is given. (Contributed by RP, 16-Jun-2021.)
Assertion
Ref Expression
clsk3nimkb ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))
Distinct variable group:   𝑘,𝑏,𝑡,𝑠

Proof of Theorem clsk3nimkb
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1oex 8215 . . . . 5 1o ∈ V
2 1n0 8221 . . . . . 6 1o ≠ ∅
3 nelsn 4581 . . . . . 6 (1o ≠ ∅ → ¬ 1o ∈ {∅})
42, 3ax-mp 5 . . . . 5 ¬ 1o ∈ {∅}
5 eldif 3876 . . . . . 6 (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6 ne0i 4249 . . . . . 6 (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
75, 6sylbir 238 . . . . 5 ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
81, 4, 7mp2an 692 . . . 4 (V ∖ {∅}) ≠ ∅
9 r19.2zb 4407 . . . 4 ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))))
108, 9mpbi 233 . . 3 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
11 rexex 3162 . . 3 (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
12 rexanali 3184 . . . . 5 (∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1312exbii 1855 . . . 4 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
14 exnal 1834 . . . 4 (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1513, 14sylbb 222 . . 3 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1610, 11, 153syl 18 . 2 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
17 difelpw 5243 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → (𝑏𝑥) ∈ 𝒫 𝑏)
1817adantr 484 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏𝑥) ∈ 𝒫 𝑏)
1918fmpttd 6932 . . . 4 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20 pwexg 5271 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
2120, 20elmapd 8522 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏))
2219, 21mpbird 260 . . 3 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏))
23 simpllr 776 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)))
24 difeq2 4031 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑏𝑥) = (𝑏𝑧))
2524cbvmptv 5158 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧))
2623, 25eqtrdi 2794 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧)))
27 difeq2 4031 . . . . . . . . 9 (𝑧 = (𝑠𝑡) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
2827adantl 485 . . . . . . . 8 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠𝑡)) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
29 simplll 775 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30 simplr 769 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
3130elpwid 4524 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠𝑏)
32 simpr 488 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
3332elpwid 4524 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡𝑏)
3431, 33unssd 4100 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ⊆ 𝑏)
3529, 34sselpwd 5219 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ∈ 𝒫 𝑏)
36 vex 3412 . . . . . . . . . 10 𝑏 ∈ V
3736difexi 5221 . . . . . . . . 9 (𝑏 ∖ (𝑠𝑡)) ∈ V
3837a1i 11 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠𝑡)) ∈ V)
3926, 28, 35, 38fvmptd 6825 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠𝑡)) = (𝑏 ∖ (𝑠𝑡)))
40 difeq2 4031 . . . . . . . . . . 11 (𝑧 = 𝑠 → (𝑏𝑧) = (𝑏𝑠))
4140adantl 485 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏𝑧) = (𝑏𝑠))
4236difexi 5221 . . . . . . . . . . 11 (𝑏𝑠) ∈ V
4342a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑠) ∈ V)
4426, 41, 30, 43fvmptd 6825 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑠) = (𝑏𝑠))
45 difeq2 4031 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑏𝑧) = (𝑏𝑡))
4645adantl 485 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏𝑧) = (𝑏𝑡))
4736difexi 5221 . . . . . . . . . . 11 (𝑏𝑡) ∈ V
4847a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑡) ∈ V)
4926, 46, 32, 48fvmptd 6825 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑡) = (𝑏𝑡))
5044, 49uneq12d 4078 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡)))
51 difindi 4196 . . . . . . . 8 (𝑏 ∖ (𝑠𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡))
5250, 51eqtr4di 2796 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (𝑏 ∖ (𝑠𝑡)))
5339, 52sseq12d 3934 . . . . . 6 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5453ralbidva 3117 . . . . 5 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5554ralbidva 3117 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5652eqeq1d 2739 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
5756imbi2d 344 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5857ralbidva 3117 . . . . . 6 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5958ralbidva 3117 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6059notbid 321 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6155, 60anbi12d 634 . . 3 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))))
62 pwidg 4535 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63 ssidd 3924 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏𝑏)
64 eldifsnneq 4704 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65 uneq1 4070 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
6665eqeq1d 2739 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏 ↔ (𝑏𝑡) = 𝑏))
67 ssequn2 4097 . . . . . . . . 9 (𝑡𝑏 ↔ (𝑏𝑡) = 𝑏)
6866, 67bitr4di 292 . . . . . . . 8 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏𝑡𝑏))
69 ineq1 4120 . . . . . . . . . . 11 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
7069difeq2d 4037 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = (𝑏 ∖ (𝑏𝑡)))
7170eqeq1d 2739 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7271notbid 321 . . . . . . . 8 (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7368, 72anbi12d 634 . . . . . . 7 (𝑠 = 𝑏 → (((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ (𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏)))
74 sseq1 3926 . . . . . . . 8 (𝑡 = 𝑏 → (𝑡𝑏𝑏𝑏))
75 ineq2 4121 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → (𝑏𝑡) = (𝑏𝑏))
76 inidm 4133 . . . . . . . . . . . . . 14 (𝑏𝑏) = 𝑏
7775, 76eqtrdi 2794 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (𝑏𝑡) = 𝑏)
7877difeq2d 4037 . . . . . . . . . . . 12 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = (𝑏𝑏))
79 difid 4285 . . . . . . . . . . . 12 (𝑏𝑏) = ∅
8078, 79eqtrdi 2794 . . . . . . . . . . 11 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = ∅)
8180eqeq1d 2739 . . . . . . . . . 10 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82 eqcom 2744 . . . . . . . . . 10 (∅ = 𝑏𝑏 = ∅)
8381, 82bitrdi 290 . . . . . . . . 9 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏𝑏 = ∅))
8483notbid 321 . . . . . . . 8 (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
8574, 84anbi12d 634 . . . . . . 7 (𝑡 = 𝑏 → ((𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏) ↔ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)))
8673, 85rspc2ev 3549 . . . . . 6 ((𝑏 ∈ 𝒫 𝑏𝑏 ∈ 𝒫 𝑏 ∧ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8762, 62, 63, 64, 86syl112anc 1376 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
88 rexanali 3184 . . . . . . 7 (∃𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8988rexbii 3170 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
90 rexnal 3160 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9189, 90sylbb 222 . . . . 5 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9287, 91syl 17 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
93 inss1 4143 . . . . . . 7 (𝑠𝑡) ⊆ 𝑠
94 ssun1 4086 . . . . . . 7 𝑠 ⊆ (𝑠𝑡)
9593, 94sstri 3910 . . . . . 6 (𝑠𝑡) ⊆ (𝑠𝑡)
96 sscon 4053 . . . . . 6 ((𝑠𝑡) ⊆ (𝑠𝑡) → (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)))
9795, 96ax-mp 5 . . . . 5 (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9897rgen2w 3074 . . . 4 𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9992, 98jctil 523 . . 3 (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
10022, 61, 99rspcedvd 3540 . 2 (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
10116, 100mprg 3075 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wal 1541   = wceq 1543  wex 1787  wcel 2110  wne 2940  wral 3061  wrex 3062  Vcvv 3408  cdif 3863  cun 3864  cin 3865  wss 3866  c0 4237  𝒫 cpw 4513  {csn 4541  cmpt 5135  wf 6376  cfv 6380  (class class class)co 7213  1oc1o 8195  m cmap 8508
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-fv 6388  df-ov 7216  df-oprab 7217  df-mpo 7218  df-1o 8202  df-map 8510
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator