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	$⊢ \neg \forall b \forall k \in ({𝒫 b}^{𝒫 b}) (\forall s \in 𝒫 b \forall t \in 𝒫 b k (s \cup t) \subseteq k (s) \cup k (t) \to \forall s \in 𝒫 b \forall t \in 𝒫 b (s \cup t = b \to k (s) \cup k (t) = b))$

Proof

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

Metamath Proof Explorer

Theorem clsk3nimkb

Proof