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 41878
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 8352 . . . . 5 1o ∈ V
2 1n0 8364 . . . . . 6 1o ≠ ∅
3 nelsn 4609 . . . . . 6 (1o ≠ ∅ → ¬ 1o ∈ {∅})
42, 3ax-mp 5 . . . . 5 ¬ 1o ∈ {∅}
5 eldif 3906 . . . . . 6 (1o ∈ (V ∖ {∅}) ↔ (1o ∈ V ∧ ¬ 1o ∈ {∅}))
6 ne0i 4278 . . . . . 6 (1o ∈ (V ∖ {∅}) → (V ∖ {∅}) ≠ ∅)
75, 6sylbir 234 . . . . 5 ((1o ∈ V ∧ ¬ 1o ∈ {∅}) → (V ∖ {∅}) ≠ ∅)
81, 4, 7mp2an 689 . . . 4 (V ∖ {∅}) ≠ ∅
9 r19.2zb 4436 . . . 4 ((V ∖ {∅}) ≠ ∅ ↔ (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))))
108, 9mpbi 229 . . 3 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
11 rexex 3077 . . 3 (∃𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
12 rexanali 3102 . . . . 5 (∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1312exbii 1849 . . . 4 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
14 exnal 1828 . . . 4 (∃𝑏 ¬ ∀𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1513, 14sylbb 218 . . 3 (∃𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
1610, 11, 153syl 18 . 2 (∀𝑏 ∈ (V ∖ {∅})∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) → ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
17 difelpw 5287 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → (𝑏𝑥) ∈ 𝒫 𝑏)
1817adantr 481 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑥 ∈ 𝒫 𝑏) → (𝑏𝑥) ∈ 𝒫 𝑏)
1918fmpttd 7026 . . . 4 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏)
20 pwexg 5314 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → 𝒫 𝑏 ∈ V)
2120, 20elmapd 8675 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ((𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏) ↔ (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)):𝒫 𝑏⟶𝒫 𝑏))
2219, 21mpbird 256 . . 3 (𝑏 ∈ (V ∖ {∅}) → (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) ∈ (𝒫 𝑏m 𝒫 𝑏))
23 simpllr 773 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)))
24 difeq2 4061 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑏𝑥) = (𝑏𝑧))
2524cbvmptv 5198 . . . . . . . . 9 (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥)) = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧))
2623, 25eqtrdi 2793 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑘 = (𝑧 ∈ 𝒫 𝑏 ↦ (𝑏𝑧)))
27 difeq2 4061 . . . . . . . . 9 (𝑧 = (𝑠𝑡) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
2827adantl 482 . . . . . . . 8 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = (𝑠𝑡)) → (𝑏𝑧) = (𝑏 ∖ (𝑠𝑡)))
29 simplll 772 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑏 ∈ (V ∖ {∅}))
30 simplr 766 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠 ∈ 𝒫 𝑏)
3130elpwid 4552 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑠𝑏)
32 simpr 485 . . . . . . . . . . 11 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡 ∈ 𝒫 𝑏)
3332elpwid 4552 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → 𝑡𝑏)
3431, 33unssd 4130 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ⊆ 𝑏)
3529, 34sselpwd 5263 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑠𝑡) ∈ 𝒫 𝑏)
36 vex 3445 . . . . . . . . . 10 𝑏 ∈ V
3736difexi 5265 . . . . . . . . 9 (𝑏 ∖ (𝑠𝑡)) ∈ V
3837a1i 11 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏 ∖ (𝑠𝑡)) ∈ V)
3926, 28, 35, 38fvmptd 6919 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘‘(𝑠𝑡)) = (𝑏 ∖ (𝑠𝑡)))
40 difeq2 4061 . . . . . . . . . . 11 (𝑧 = 𝑠 → (𝑏𝑧) = (𝑏𝑠))
4140adantl 482 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑠) → (𝑏𝑧) = (𝑏𝑠))
4236difexi 5265 . . . . . . . . . . 11 (𝑏𝑠) ∈ V
4342a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑠) ∈ V)
4426, 41, 30, 43fvmptd 6919 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑠) = (𝑏𝑠))
45 difeq2 4061 . . . . . . . . . . 11 (𝑧 = 𝑡 → (𝑏𝑧) = (𝑏𝑡))
4645adantl 482 . . . . . . . . . 10 (((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) ∧ 𝑧 = 𝑡) → (𝑏𝑧) = (𝑏𝑡))
4736difexi 5265 . . . . . . . . . . 11 (𝑏𝑡) ∈ V
4847a1i 11 . . . . . . . . . 10 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑏𝑡) ∈ V)
4926, 46, 32, 48fvmptd 6919 . . . . . . . . 9 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (𝑘𝑡) = (𝑏𝑡))
5044, 49uneq12d 4108 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡)))
51 difindi 4225 . . . . . . . 8 (𝑏 ∖ (𝑠𝑡)) = ((𝑏𝑠) ∪ (𝑏𝑡))
5250, 51eqtr4di 2795 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘𝑠) ∪ (𝑘𝑡)) = (𝑏 ∖ (𝑠𝑡)))
5339, 52sseq12d 3963 . . . . . 6 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → ((𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5453ralbidva 3169 . . . . 5 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5554ralbidva 3169 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))))
5652eqeq1d 2739 . . . . . . . 8 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
5756imbi2d 340 . . . . . . 7 ((((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) ∧ 𝑡 ∈ 𝒫 𝑏) → (((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5857ralbidva 3169 . . . . . 6 (((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) ∧ 𝑠 ∈ 𝒫 𝑏) → (∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
5958ralbidva 3169 . . . . 5 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6059notbid 317 . . . 4 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → (¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
6155, 60anbi12d 631 . . 3 ((𝑏 ∈ (V ∖ {∅}) ∧ 𝑘 = (𝑥 ∈ 𝒫 𝑏 ↦ (𝑏𝑥))) → ((∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)) ↔ (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))))
62 pwidg 4563 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏 ∈ 𝒫 𝑏)
63 ssidd 3953 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → 𝑏𝑏)
64 eldifsnneq 4734 . . . . . 6 (𝑏 ∈ (V ∖ {∅}) → ¬ 𝑏 = ∅)
65 uneq1 4100 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
6665eqeq1d 2739 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏 ↔ (𝑏𝑡) = 𝑏))
67 ssequn2 4127 . . . . . . . . 9 (𝑡𝑏 ↔ (𝑏𝑡) = 𝑏)
6866, 67bitr4di 288 . . . . . . . 8 (𝑠 = 𝑏 → ((𝑠𝑡) = 𝑏𝑡𝑏))
69 ineq1 4149 . . . . . . . . . . 11 (𝑠 = 𝑏 → (𝑠𝑡) = (𝑏𝑡))
7069difeq2d 4067 . . . . . . . . . 10 (𝑠 = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = (𝑏 ∖ (𝑏𝑡)))
7170eqeq1d 2739 . . . . . . . . 9 (𝑠 = 𝑏 → ((𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7271notbid 317 . . . . . . . 8 (𝑠 = 𝑏 → (¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏 ↔ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏))
7368, 72anbi12d 631 . . . . . . 7 (𝑠 = 𝑏 → (((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ (𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏)))
74 sseq1 3955 . . . . . . . 8 (𝑡 = 𝑏 → (𝑡𝑏𝑏𝑏))
75 ineq2 4150 . . . . . . . . . . . . . 14 (𝑡 = 𝑏 → (𝑏𝑡) = (𝑏𝑏))
76 inidm 4162 . . . . . . . . . . . . . 14 (𝑏𝑏) = 𝑏
7775, 76eqtrdi 2793 . . . . . . . . . . . . 13 (𝑡 = 𝑏 → (𝑏𝑡) = 𝑏)
7877difeq2d 4067 . . . . . . . . . . . 12 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = (𝑏𝑏))
79 difid 4314 . . . . . . . . . . . 12 (𝑏𝑏) = ∅
8078, 79eqtrdi 2793 . . . . . . . . . . 11 (𝑡 = 𝑏 → (𝑏 ∖ (𝑏𝑡)) = ∅)
8180eqeq1d 2739 . . . . . . . . . 10 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ∅ = 𝑏))
82 eqcom 2744 . . . . . . . . . 10 (∅ = 𝑏𝑏 = ∅)
8381, 82bitrdi 286 . . . . . . . . 9 (𝑡 = 𝑏 → ((𝑏 ∖ (𝑏𝑡)) = 𝑏𝑏 = ∅))
8483notbid 317 . . . . . . . 8 (𝑡 = 𝑏 → (¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏 ↔ ¬ 𝑏 = ∅))
8574, 84anbi12d 631 . . . . . . 7 (𝑡 = 𝑏 → ((𝑡𝑏 ∧ ¬ (𝑏 ∖ (𝑏𝑡)) = 𝑏) ↔ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)))
8673, 85rspc2ev 3581 . . . . . 6 ((𝑏 ∈ 𝒫 𝑏𝑏 ∈ 𝒫 𝑏 ∧ (𝑏𝑏 ∧ ¬ 𝑏 = ∅)) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8762, 62, 63, 64, 86syl112anc 1373 . . . . 5 (𝑏 ∈ (V ∖ {∅}) → ∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏))
88 rexanali 3102 . . . . . . 7 (∃𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
8988rexbii 3094 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
90 rexnal 3100 . . . . . 6 (∃𝑠 ∈ 𝒫 𝑏 ¬ ∀𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏) ↔ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9189, 90sylbb 218 . . . . 5 (∃𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 ∧ ¬ (𝑏 ∖ (𝑠𝑡)) = 𝑏) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
9287, 91syl 17 . . . 4 (𝑏 ∈ (V ∖ {∅}) → ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏))
93 inss1 4172 . . . . . . 7 (𝑠𝑡) ⊆ 𝑠
94 ssun1 4116 . . . . . . 7 𝑠 ⊆ (𝑠𝑡)
9593, 94sstri 3939 . . . . . 6 (𝑠𝑡) ⊆ (𝑠𝑡)
96 sscon 4083 . . . . . 6 ((𝑠𝑡) ⊆ (𝑠𝑡) → (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)))
9795, 96ax-mp 5 . . . . 5 (𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9897rgen2w 3067 . . . 4 𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡))
9992, 98jctil 520 . . 3 (𝑏 ∈ (V ∖ {∅}) → (∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑏 ∖ (𝑠𝑡)) ⊆ (𝑏 ∖ (𝑠𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → (𝑏 ∖ (𝑠𝑡)) = 𝑏)))
10022, 61, 99rspcedvd 3572 . 2 (𝑏 ∈ (V ∖ {∅}) → ∃𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) ∧ ¬ ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏)))
10116, 100mprg 3068 1 ¬ ∀𝑏𝑘 ∈ (𝒫 𝑏m 𝒫 𝑏)(∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠𝑡)) ⊆ ((𝑘𝑠) ∪ (𝑘𝑡)) → ∀𝑠 ∈ 𝒫 𝑏𝑡 ∈ 𝒫 𝑏((𝑠𝑡) = 𝑏 → ((𝑘𝑠) ∪ (𝑘𝑡)) = 𝑏))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wal 1538   = wceq 1540  wex 1780  wcel 2105  wne 2941  wral 3062  wrex 3071  Vcvv 3441  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  𝒫 cpw 4543  {csn 4569  cmpt 5168  wf 6459  cfv 6463  (class class class)co 7313  1oc1o 8335  m cmap 8661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5236  ax-nul 5243  ax-pow 5301  ax-pr 5365  ax-un 7626
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3443  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4470  df-pw 4545  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4849  df-br 5086  df-opab 5148  df-mpt 5169  df-id 5505  df-xp 5611  df-rel 5612  df-cnv 5613  df-co 5614  df-dm 5615  df-rn 5616  df-res 5617  df-ima 5618  df-suc 6292  df-iota 6415  df-fun 6465  df-fn 6466  df-f 6467  df-fv 6471  df-ov 7316  df-oprab 7317  df-mpo 7318  df-1o 8342  df-map 8663
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator