Metamath Proof Explorer

Theorem clsk3nimkb

Description: If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of k = ( x e. ~P b |-> ( b \ x ) ) is given. (Contributed by RP, 16-Jun-2021)

Ref Expression
Assertion clsk3nimkb ⊢¬∀b∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b

Proof

Step Hyp Ref Expression
1 1oex ⊢1𝑜∈V
2 1n0 ⊢1𝑜≠∅
3 nelsn ⊢1𝑜≠∅→¬1𝑜∈∅
4 2 3 ax-mp ⊢¬1𝑜∈∅
5 eldif ⊢1𝑜∈V∖∅↔1𝑜∈V∧¬1𝑜∈∅
6 ne0i ⊢1𝑜∈V∖∅→V∖∅≠∅
7 5 6 sylbir ⊢1𝑜∈V∧¬1𝑜∈∅→V∖∅≠∅
8 1 4 7 mp2an ⊢V∖∅≠∅
9 r19.2zb ⊢V∖∅≠∅↔∀b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b→∃b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
10 8 9 mpbi ⊢∀b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b→∃b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
11 rexex ⊢∃b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b→∃b∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
12 rexanali ⊢∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔¬∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
13 12 exbii ⊢∃b∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔∃b¬∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
14 exnal ⊢∃b¬∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔¬∀b∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
15 13 14 sylbb ⊢∃b∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b→¬∀b∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
16 10 11 15 3syl ⊢∀b∈V∖∅∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b→¬∀b∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
17 difelpw ⊢b∈V∖∅→b∖x∈𝒫b
18 17 adantr ⊢b∈V∖∅∧x∈𝒫b→b∖x∈𝒫b
19 18 fmpttd ⊢b∈V∖∅→x∈𝒫b⟼b∖x:𝒫b⟶𝒫b
20 pwexg ⊢b∈V∖∅→𝒫b∈V
21 20 20 elmapd ⊢b∈V∖∅→x∈𝒫b⟼b∖x∈𝒫b𝒫b↔x∈𝒫b⟼b∖x:𝒫b⟶𝒫b
22 19 21 mpbird ⊢b∈V∖∅→x∈𝒫b⟼b∖x∈𝒫b𝒫b
23 simpllr ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k=x∈𝒫b⟼b∖x
24 difeq2 ⊢x=z→b∖x=b∖z
25 24 cbvmptv ⊢x∈𝒫b⟼b∖x=z∈𝒫b⟼b∖z
26 23 25 eqtrdi ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k=z∈𝒫b⟼b∖z
27 difeq2 ⊢z=s∪t→b∖z=b∖s∪t
28 27 adantl ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b∧z=s∪t→b∖z=b∖s∪t
29 simplll ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→b∈V∖∅
30 simplr ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→s∈𝒫b
31 30 elpwid ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→s⊆b
32 simpr ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→t∈𝒫b
33 32 elpwid ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→t⊆b
34 31 33 unssd ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→s∪t⊆b
35 29 34 sselpwd ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→s∪t∈𝒫b
36 vex ⊢b∈V
37 36 difexi ⊢b∖s∪t∈V
38 37 a1i ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→b∖s∪t∈V
39 26 28 35 38 fvmptd ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s∪t=b∖s∪t
40 difeq2 ⊢z=s→b∖z=b∖s
41 40 adantl ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b∧z=s→b∖z=b∖s
42 36 difexi ⊢b∖s∈V
43 42 a1i ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→b∖s∈V
44 26 41 30 43 fvmptd ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s=b∖s
45 difeq2 ⊢z=t→b∖z=b∖t
46 45 adantl ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b∧z=t→b∖z=b∖t
47 36 difexi ⊢b∖t∈V
48 47 a1i ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→b∖t∈V
49 26 46 32 48 fvmptd ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡t=b∖t
50 44 49 uneq12d ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s∪k⁡t=b∖s∪b∖t
51 difindi ⊢b∖s∩t=b∖s∪b∖t
52 50 51 eqtr4di ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s∪k⁡t=b∖s∩t
53 39 52 sseq12d ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s∪t⊆k⁡s∪k⁡t↔b∖s∪t⊆b∖s∩t
54 53 ralbidva ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b→∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t↔∀t∈𝒫bb∖s∪t⊆b∖s∩t
55 54 ralbidva ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x→∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t↔∀s∈𝒫b∀t∈𝒫bb∖s∪t⊆b∖s∩t
56 52 eqeq1d ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→k⁡s∪k⁡t=b↔b∖s∩t=b
57 56 imbi2d ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b∧t∈𝒫b→s∪t=b→k⁡s∪k⁡t=b↔s∪t=b→b∖s∩t=b
58 57 ralbidva ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x∧s∈𝒫b→∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔∀t∈𝒫bs∪t=b→b∖s∩t=b
59 58 ralbidva ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
60 59 notbid ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x→¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
61 55 60 anbi12d ⊢b∈V∖∅∧k=x∈𝒫b⟼b∖x→∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b↔∀s∈𝒫b∀t∈𝒫bb∖s∪t⊆b∖s∩t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
62 pwidg ⊢b∈V∖∅→b∈𝒫b
63 ssidd ⊢b∈V∖∅→b⊆b
64 eldifsnneq ⊢b∈V∖∅→¬b=∅
65 uneq1 ⊢s=b→s∪t=b∪t
66 65 eqeq1d ⊢s=b→s∪t=b↔b∪t=b
67 ssequn2 ⊢t⊆b↔b∪t=b
68 66 67 bitr4di ⊢s=b→s∪t=b↔t⊆b
69 ineq1 ⊢s=b→s∩t=b∩t
70 69 difeq2d ⊢s=b→b∖s∩t=b∖b∩t
71 70 eqeq1d ⊢s=b→b∖s∩t=b↔b∖b∩t=b
72 71 notbid ⊢s=b→¬b∖s∩t=b↔¬b∖b∩t=b
73 68 72 anbi12d ⊢s=b→s∪t=b∧¬b∖s∩t=b↔t⊆b∧¬b∖b∩t=b
74 sseq1 ⊢t=b→t⊆b↔b⊆b
75 ineq2 ⊢t=b→b∩t=b∩b
76 inidm ⊢b∩b=b
77 75 76 eqtrdi ⊢t=b→b∩t=b
78 77 difeq2d ⊢t=b→b∖b∩t=b∖b
79 difid ⊢b∖b=∅
80 78 79 eqtrdi ⊢t=b→b∖b∩t=∅
81 80 eqeq1d ⊢t=b→b∖b∩t=b↔∅=b
82 eqcom ⊢∅=b↔b=∅
83 81 82 bitrdi ⊢t=b→b∖b∩t=b↔b=∅
84 83 notbid ⊢t=b→¬b∖b∩t=b↔¬b=∅
85 74 84 anbi12d ⊢t=b→t⊆b∧¬b∖b∩t=b↔b⊆b∧¬b=∅
86 73 85 rspc2ev ⊢b∈𝒫b∧b∈𝒫b∧b⊆b∧¬b=∅→∃s∈𝒫b∃t∈𝒫bs∪t=b∧¬b∖s∩t=b
87 62 62 63 64 86 syl112anc ⊢b∈V∖∅→∃s∈𝒫b∃t∈𝒫bs∪t=b∧¬b∖s∩t=b
88 rexanali ⊢∃t∈𝒫bs∪t=b∧¬b∖s∩t=b↔¬∀t∈𝒫bs∪t=b→b∖s∩t=b
89 88 rexbii ⊢∃s∈𝒫b∃t∈𝒫bs∪t=b∧¬b∖s∩t=b↔∃s∈𝒫b¬∀t∈𝒫bs∪t=b→b∖s∩t=b
90 rexnal ⊢∃s∈𝒫b¬∀t∈𝒫bs∪t=b→b∖s∩t=b↔¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
91 89 90 sylbb ⊢∃s∈𝒫b∃t∈𝒫bs∪t=b∧¬b∖s∩t=b→¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
92 87 91 syl ⊢b∈V∖∅→¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
93 inss1 ⊢s∩t⊆s
94 ssun1 ⊢s⊆s∪t
95 93 94 sstri ⊢s∩t⊆s∪t
96 sscon ⊢s∩t⊆s∪t→b∖s∪t⊆b∖s∩t
97 95 96 ax-mp ⊢b∖s∪t⊆b∖s∩t
98 97 rgen2w ⊢∀s∈𝒫b∀t∈𝒫bb∖s∪t⊆b∖s∩t
99 92 98 jctil ⊢b∈V∖∅→∀s∈𝒫b∀t∈𝒫bb∖s∪t⊆b∖s∩t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→b∖s∩t=b
100 22 61 99 rspcedvd ⊢b∈V∖∅→∃k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t∧¬∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b
101 16 100 mprg ⊢¬∀b∀k∈𝒫b𝒫b∀s∈𝒫b∀t∈𝒫bk⁡s∪t⊆k⁡s∪k⁡t→∀s∈𝒫b∀t∈𝒫bs∪t=b→k⁡s∪k⁡t=b