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 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s 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 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b
10 8 9 mpbi b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b
11 rexex b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b
12 rexanali k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b ¬ k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b
13 12 exbii b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b b ¬ k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b
14 exnal b ¬ k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b ¬ b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b
15 13 14 sylbb b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b ¬ b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b
16 10 11 15 3syl b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b ¬ b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s 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 𝒫 b k s t k s k t t 𝒫 b b s t b s t
55 54 ralbidva b V k = x 𝒫 b b x s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b b 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 𝒫 b s t = b k s k t = b t 𝒫 b s t = b b s t = b
59 58 ralbidva b V k = x 𝒫 b b x s 𝒫 b t 𝒫 b s t = b k s k t = b s 𝒫 b t 𝒫 b s t = b b s t = b
60 59 notbid b V k = x 𝒫 b b x ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b ¬ s 𝒫 b t 𝒫 b s t = b b s t = b
61 55 60 anbi12d b V k = x 𝒫 b b x s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b s 𝒫 b t 𝒫 b b s t b s t ¬ s 𝒫 b t 𝒫 b s 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 𝒫 b s t = b ¬ b s t = b
87 62 62 63 64 86 syl112anc b V s 𝒫 b t 𝒫 b s t = b ¬ b s t = b
88 rexanali t 𝒫 b s t = b ¬ b s t = b ¬ t 𝒫 b s t = b b s t = b
89 88 rexbii s 𝒫 b t 𝒫 b s t = b ¬ b s t = b s 𝒫 b ¬ t 𝒫 b s t = b b s t = b
90 rexnal s 𝒫 b ¬ t 𝒫 b s t = b b s t = b ¬ s 𝒫 b t 𝒫 b s t = b b s t = b
91 89 90 sylbb s 𝒫 b t 𝒫 b s t = b ¬ b s t = b ¬ s 𝒫 b t 𝒫 b s t = b b s t = b
92 87 91 syl b V ¬ s 𝒫 b t 𝒫 b s 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 𝒫 b b s t b s t
99 92 98 jctil b V s 𝒫 b t 𝒫 b b s t b s t ¬ s 𝒫 b t 𝒫 b s t = b b s t = b
100 22 61 99 rspcedvd b V k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t ¬ s 𝒫 b t 𝒫 b s t = b k s k t = b
101 16 100 mprg ¬ b k 𝒫 b 𝒫 b s 𝒫 b t 𝒫 b k s t k s k t s 𝒫 b t 𝒫 b s t = b k s k t = b