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

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

Proof of Theorem clsk3nimkb
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1on 7454 . . . . . 6 1𝑜 ∈ On
21elexi 3186 . . . . 5 1𝑜 ∈ V
3 1n0 7462 . . . . . 6 1𝑜 ≠ ∅
4 nelsn 4159 . . . . . 6 (1𝑜 ≠ ∅ → ¬ 1𝑜 ∈ {∅})
53, 4ax-mp 5 . . . . 5 ¬ 1𝑜 ∈ {∅}
6 eldif 3550 . . . . . 6 (1𝑜 ∈ (V ∖ {∅}) ↔ (1𝑜 ∈ V ∧ ¬ 1𝑜 ∈ {∅}))
7 ne0i 3880 . . . . . 6 (1𝑜 ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
86, 7sylbir 224 . . . . 5 ((1𝑜 ∈ V ∧ ¬ 1𝑜 ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
92, 5, 8mp2an 704 . . . 4 (V ∖ {∅}) ≠ ∅
10 r19.2zb 4013 . . . 4 ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))))
119, 10mpbi 219 . . 3 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
12 rexex 2985 . . 3 (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
13 rexanali 2981 . . . . 5 (∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1413exbii 1764 . . . 4 (∃𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
15 exnal 1744 . . . 4 (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1614, 15sylbb 208 . . 3 (∃𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1711, 12, 163syl 18 . 2 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
18 id 22 . . . . . . 7 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ (V ∖ {∅}))
19 difssd 3700 . . . . . . 7 (𝑏 ∈ (V ∖ {∅}) → (𝑏𝑥) ⊆ 𝑏)
2018, 19sselpwd 4734 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → (𝑏𝑥) ∈ 𝒫 𝑏)
2120adantr 480 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏𝑥) ∈ 𝒫 𝑏)
22 eqid 2610 . . . . 5 (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))
2321, 22fmptd 6292 . . . 4 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏)
24 pwexg 4776 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
2524, 24elmapd 7758 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏𝑚 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏))
2623, 25mpbird 246 . . 3 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏𝑚 𝒫 𝑏))
27 simpllr 795 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)))
28 difeq2 3684 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑏𝑥) = (𝑏𝑧))
2928cbvmptv 4678 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧))
3027, 29syl6eq 2660 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧)))
31 difeq2 3684 . . . . . . . . 9 (𝑧 = (𝑠𝑡) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
3231adantl 481 . . . . . . . 8 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠𝑡)) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
33 simplll 794 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
34 simplr 788 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
3534elpwid 4118 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠𝑏)
36 simpr 476 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
3736elpwid 4118 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡𝑏)
3835, 37unssd 3751 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ⊆ 𝑏)
3933, 38sselpwd 4734 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ∈ 𝒫 𝑏)
40 vex 3176 . . . . . . . . . 10 𝑏 ∈ V
4140difexi 4736 . . . . . . . . 9 (𝑏 ∖ (𝑠𝑡)) ∈ V
4241a1i 11 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠𝑡)) ∈ V)
4330, 32, 39, 42fvmptd 6197 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠𝑡)) = (𝑏 ∖ (𝑠𝑡)))
44 difeq2 3684 . . . . . . . . . . 11 (𝑧 = 𝑠 → (𝑏𝑧) = (𝑏𝑠))
4544adantl 481 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏𝑧) = (𝑏𝑠))
4640difexi 4736 . . . . . . . . . . 11 (𝑏𝑠) ∈ V
4746a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑠) ∈ V)
4830, 45, 34, 47fvmptd 6197 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑠) = (𝑏𝑠))
49 difeq2 3684 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑏𝑧) = (𝑏𝑡))
5049adantl 481 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏𝑧) = (𝑏𝑡))
5140difexi 4736 . . . . . . . . . . 11 (𝑏𝑡) ∈ V
5251a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑡) ∈ V)
5330, 50, 36, 52fvmptd 6197 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑡) = (𝑏𝑡))
5448, 53uneq12d 3730 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡)))
55 difindi 3840 . . . . . . . 8 (𝑏 ∖ (𝑠𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡))
5654, 55syl6eqr 2662 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (𝑏 ∖ (𝑠𝑡)))
5743, 56sseq12d 3597 . . . . . 6 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5857ralbidva 2968 . . . . 5 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5958ralbidva 2968 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
6056eqeq1d 2612 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
6160imbi2d 329 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6261ralbidva 2968 . . . . . 6 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6362ralbidva 2968 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6463notbid 307 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6559, 64anbi12d 743 . . 3 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))))
66 pwidg 4121 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
67 ssid 3587 . . . . . . 7 𝑏𝑏
6867a1i 11 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏𝑏)
69 eldifsni 4261 . . . . . . 7 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ≠ ∅)
7069neneqd 2787 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
71 uneq1 3722 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
7271eqeq1d 2612 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏 ↔ (𝑏𝑡) = 𝑏))
73 ssequn2 3748 . . . . . . . . 9 (𝑡𝑏 ↔ (𝑏𝑡) = 𝑏)
7472, 73syl6bbr 277 . . . . . . . 8 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏𝑡𝑏))
75 ineq1 3769 . . . . . . . . . . 11 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
7675difeq2d 3690 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = (𝑏 ∖ (𝑏𝑡)))
7776eqeq1d 2612 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7877notbid 307 . . . . . . . 8 (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7974, 78anbi12d 743 . . . . . . 7 (𝑠 = 𝑏 → (((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ (𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏)))
80 sseq1 3589 . . . . . . . 8 (𝑡 = 𝑏 → (𝑡𝑏𝑏𝑏))
81 ineq2 3770 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → (𝑏𝑡) = (𝑏𝑏))
82 inidm 3784 . . . . . . . . . . . . . 14 (𝑏𝑏) = 𝑏
8381, 82syl6eq 2660 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (𝑏𝑡) = 𝑏)
8483difeq2d 3690 . . . . . . . . . . . 12 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = (𝑏𝑏))
85 difid 3902 . . . . . . . . . . . 12 (𝑏𝑏) = ∅
8684, 85syl6eq 2660 . . . . . . . . . . 11 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = ∅)
8786eqeq1d 2612 . . . . . . . . . 10 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ∅ = 𝑏))
88 eqcom 2617 . . . . . . . . . 10 (∅ = 𝑏𝑏 = ∅)
8987, 88syl6bb 275 . . . . . . . . 9 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏𝑏 = ∅))
9089notbid 307 . . . . . . . 8 (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
9180, 90anbi12d 743 . . . . . . 7 (𝑡 = 𝑏 → ((𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏) ↔ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)))
9279, 91rspc2ev 3295 . . . . . 6 ((𝑏 ∈ 𝒫 𝑏𝑏 ∈ 𝒫 𝑏 ∧ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9366, 66, 68, 70, 92syl112anc 1322 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
94 rexanali 2981 . . . . . . 7 (∃𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9594rexbii 3023 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
96 rexnal 2978 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9795, 96sylbb 208 . . . . 5 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9893, 97syl 17 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
99 inss1 3795 . . . . . . 7 (𝑠𝑡) ⊆ 𝑠
100 ssun1 3738 . . . . . . 7 𝑠 ⊆ (𝑠𝑡)
10199, 100sstri 3577 . . . . . 6 (𝑠𝑡) ⊆ (𝑠𝑡)
102 sscon 3706 . . . . . 6 ((𝑠𝑡) ⊆ (𝑠𝑡) → (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)))
103101, 102ax-mp 5 . . . . 5 (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
104103rgen2w 2909 . . . 4 𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
10598, 104jctil 558 . . 3 (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
10626, 65, 105rspcedvd 3289 . 2 (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
10717, 106mprg 2910 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏𝑚 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125   ↦ cmpt 4643  Oncon0 5640  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  1𝑜c1o 7440   ↑𝑚 cmap 7744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-1o 7447  df-map 7746 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator