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

Theorem clsk3nimkb 40786
 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 8096 . . . . 5 1o ∈ V
2 1n0 8105 . . . . . 6 1o ≠ ∅
3 nelsn 4565 . . . . . 6 (1o ≠ ∅ → ¬ 1o ∈ {∅})
42, 3ax-mp 5 . . . . 5 ¬ 1o ∈ {∅}
5 eldif 3891 . . . . . 6 (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6 ne0i 4250 . . . . . 6 (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
75, 6sylbir 238 . . . . 5 ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
81, 4, 7mp2an 691 . . . 4 (V ∖ {∅}) ≠ ∅
9 r19.2zb 4399 . . . 4 ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))))
108, 9mpbi 233 . . 3 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
11 rexex 3203 . . 3 (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
12 rexanali 3224 . . . . 5 (∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1312exbii 1849 . . . 4 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
14 exnal 1828 . . . 4 (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1513, 14sylbb 222 . . 3 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1610, 11, 153syl 18 . 2 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
17 difelpw 5218 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → (𝑏𝑥) ∈ 𝒫 𝑏)
1817adantr 484 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏𝑥) ∈ 𝒫 𝑏)
1918fmpttd 6857 . . . 4 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20 pwexg 5245 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
2120, 20elmapd 8406 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏))
2219, 21mpbird 260 . . 3 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏))
23 simpllr 775 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)))
24 difeq2 4044 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑏𝑥) = (𝑏𝑧))
2524cbvmptv 5134 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧))
2623, 25eqtrdi 2849 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧)))
27 difeq2 4044 . . . . . . . . 9 (𝑧 = (𝑠𝑡) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
2827adantl 485 . . . . . . . 8 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠𝑡)) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
29 simplll 774 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30 simplr 768 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
3130elpwid 4508 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠𝑏)
32 simpr 488 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
3332elpwid 4508 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡𝑏)
3431, 33unssd 4113 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ⊆ 𝑏)
3529, 34sselpwd 5195 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ∈ 𝒫 𝑏)
36 vex 3444 . . . . . . . . . 10 𝑏 ∈ V
3736difexi 5197 . . . . . . . . 9 (𝑏 ∖ (𝑠𝑡)) ∈ V
3837a1i 11 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠𝑡)) ∈ V)
3926, 28, 35, 38fvmptd 6753 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠𝑡)) = (𝑏 ∖ (𝑠𝑡)))
40 difeq2 4044 . . . . . . . . . . 11 (𝑧 = 𝑠 → (𝑏𝑧) = (𝑏𝑠))
4140adantl 485 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏𝑧) = (𝑏𝑠))
4236difexi 5197 . . . . . . . . . . 11 (𝑏𝑠) ∈ V
4342a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑠) ∈ V)
4426, 41, 30, 43fvmptd 6753 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑠) = (𝑏𝑠))
45 difeq2 4044 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑏𝑧) = (𝑏𝑡))
4645adantl 485 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏𝑧) = (𝑏𝑡))
4736difexi 5197 . . . . . . . . . . 11 (𝑏𝑡) ∈ V
4847a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑡) ∈ V)
4926, 46, 32, 48fvmptd 6753 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑡) = (𝑏𝑡))
5044, 49uneq12d 4091 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡)))
51 difindi 4208 . . . . . . . 8 (𝑏 ∖ (𝑠𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡))
5250, 51eqtr4di 2851 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (𝑏 ∖ (𝑠𝑡)))
5339, 52sseq12d 3948 . . . . . 6 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5453ralbidva 3161 . . . . 5 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5554ralbidva 3161 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5652eqeq1d 2800 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
5756imbi2d 344 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5857ralbidva 3161 . . . . . 6 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5958ralbidva 3161 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6059notbid 321 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6155, 60anbi12d 633 . . 3 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))))
62 pwidg 4519 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63 ssidd 3938 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏𝑏)
64 eldifsnneq 4684 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65 uneq1 4083 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
6665eqeq1d 2800 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏 ↔ (𝑏𝑡) = 𝑏))
67 ssequn2 4110 . . . . . . . . 9 (𝑡𝑏 ↔ (𝑏𝑡) = 𝑏)
6866, 67bitr4di 292 . . . . . . . 8 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏𝑡𝑏))
69 ineq1 4131 . . . . . . . . . . 11 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
7069difeq2d 4050 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = (𝑏 ∖ (𝑏𝑡)))
7170eqeq1d 2800 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7271notbid 321 . . . . . . . 8 (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7368, 72anbi12d 633 . . . . . . 7 (𝑠 = 𝑏 → (((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ (𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏)))
74 sseq1 3940 . . . . . . . 8 (𝑡 = 𝑏 → (𝑡𝑏𝑏𝑏))
75 ineq2 4133 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → (𝑏𝑡) = (𝑏𝑏))
76 inidm 4145 . . . . . . . . . . . . . 14 (𝑏𝑏) = 𝑏
7775, 76eqtrdi 2849 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (𝑏𝑡) = 𝑏)
7877difeq2d 4050 . . . . . . . . . . . 12 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = (𝑏𝑏))
79 difid 4284 . . . . . . . . . . . 12 (𝑏𝑏) = ∅
8078, 79eqtrdi 2849 . . . . . . . . . . 11 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = ∅)
8180eqeq1d 2800 . . . . . . . . . 10 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82 eqcom 2805 . . . . . . . . . 10 (∅ = 𝑏𝑏 = ∅)
8381, 82syl6bb 290 . . . . . . . . 9 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏𝑏 = ∅))
8483notbid 321 . . . . . . . 8 (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
8574, 84anbi12d 633 . . . . . . 7 (𝑡 = 𝑏 → ((𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏) ↔ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)))
8673, 85rspc2ev 3583 . . . . . 6 ((𝑏 ∈ 𝒫 𝑏𝑏 ∈ 𝒫 𝑏 ∧ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8762, 62, 63, 64, 86syl112anc 1371 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
88 rexanali 3224 . . . . . . 7 (∃𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8988rexbii 3210 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
90 rexnal 3201 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9189, 90sylbb 222 . . . . 5 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9287, 91syl 17 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
93 inss1 4155 . . . . . . 7 (𝑠𝑡) ⊆ 𝑠
94 ssun1 4099 . . . . . . 7 𝑠 ⊆ (𝑠𝑡)
9593, 94sstri 3924 . . . . . 6 (𝑠𝑡) ⊆ (𝑠𝑡)
96 sscon 4066 . . . . . 6 ((𝑠𝑡) ⊆ (𝑠𝑡) → (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)))
9795, 96ax-mp 5 . . . . 5 (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9897rgen2w 3119 . . . 4 𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9992, 98jctil 523 . . 3 (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
10022, 61, 99rspcedvd 3574 . 2 (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
10116, 100mprg 3120 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525   ↦ cmpt 5111  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136  1oc1o 8081   ↑m cmap 8392 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-ord 6163  df-on 6164  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-1o 8088  df-map 8394 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator