clsk1indlem1

Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) does not have the K1 property of isotony. (Contributed by RP, 6-Jul-2021)

		Ref	Expression
	Hypothesis	clsk1indlem.k	$⊢ K = (r \in 𝒫 3_{𝑜} ⟼ if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r))$
	Assertion	clsk1indlem1	$⊢ \exists s \in 𝒫 3_{𝑜} \exists t \in 𝒫 3_{𝑜} (s \subseteq t \land \neg K (s) \subseteq K (t))$

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	$⊢ K = (r \in 𝒫 3_{𝑜} ⟼ if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r))$
2		tpex	$⊢ \{\emptyset, 1_{𝑜}, 2_{𝑜}\} \in V$
3		snsstp1	$⊢ \{\emptyset\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
4	2 3	elpwi2	$⊢ \{\emptyset\} \in 𝒫 \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
5		df3o2	$⊢ 3_{𝑜} = \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
6	5	pweqi	$⊢ 𝒫 3_{𝑜} = 𝒫 \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
7	4 6	eleqtrri	$⊢ \{\emptyset\} \in 𝒫 3_{𝑜}$
8	2	a1i	$⊢ ⊤ \to \{\emptyset, 1_{𝑜}, 2_{𝑜}\} \in V$
9	3	a1i	$⊢ ⊤ \to \{\emptyset\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
10		0ex	$⊢ \emptyset \in V$
11	10	snss	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}, 2_{𝑜}\} \leftrightarrow \{\emptyset\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
12	9 11	sylibr	$⊢ ⊤ \to \emptyset \in \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
13		snsstp3	$⊢ \{2_{𝑜}\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
14	13	a1i	$⊢ ⊤ \to \{2_{𝑜}\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
15		2oex	$⊢ 2_{𝑜} \in V$
16	15	snss	$⊢ 2_{𝑜} \in \{\emptyset, 1_{𝑜}, 2_{𝑜}\} \leftrightarrow \{2_{𝑜}\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
17	14 16	sylibr	$⊢ ⊤ \to 2_{𝑜} \in \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
18	12 17	prssd	$⊢ ⊤ \to \{\emptyset, 2_{𝑜}\} \subseteq \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
19	8 18	sselpwd	$⊢ ⊤ \to \{\emptyset, 2_{𝑜}\} \in 𝒫 \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
20	19	mptru	$⊢ \{\emptyset, 2_{𝑜}\} \in 𝒫 \{\emptyset, 1_{𝑜}, 2_{𝑜}\}$
21	20 6	eleqtrri	$⊢ \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}$
22		simpl	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \{\emptyset\} \in 𝒫 3_{𝑜}$
23		sseq1	$⊢ s = \{\emptyset\} \to (s \subseteq t \leftrightarrow \{\emptyset\} \subseteq t)$
24		fveq2	$⊢ s = \{\emptyset\} \to K (s) = K (\{\emptyset\})$
25	24	sseq1d	$⊢ s = \{\emptyset\} \to (K (s) \subseteq K (t) \leftrightarrow K (\{\emptyset\}) \subseteq K (t))$
26	25	notbid	$⊢ s = \{\emptyset\} \to (\neg K (s) \subseteq K (t) \leftrightarrow \neg K (\{\emptyset\}) \subseteq K (t))$
27	23 26	anbi12d	$⊢ s = \{\emptyset\} \to ((s \subseteq t \land \neg K (s) \subseteq K (t)) \leftrightarrow (\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t)))$
28	27	rexbidv	$⊢ s = \{\emptyset\} \to (\exists t \in 𝒫 3_{𝑜} (s \subseteq t \land \neg K (s) \subseteq K (t)) \leftrightarrow \exists t \in 𝒫 3_{𝑜} (\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t)))$
29	28	adantl	$⊢ ((\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \land s = \{\emptyset\}) \to (\exists t \in 𝒫 3_{𝑜} (s \subseteq t \land \neg K (s) \subseteq K (t)) \leftrightarrow \exists t \in 𝒫 3_{𝑜} (\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t)))$
30		simpr	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}$
31		fveq2	$⊢ t = \{\emptyset, 2_{𝑜}\} \to K (t) = K (\{\emptyset, 2_{𝑜}\})$
32	31	sseq2d	$⊢ t = \{\emptyset, 2_{𝑜}\} \to (K (\{\emptyset\}) \subseteq K (t) \leftrightarrow K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\}))$
33	32	notbid	$⊢ t = \{\emptyset, 2_{𝑜}\} \to (\neg K (\{\emptyset\}) \subseteq K (t) \leftrightarrow \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\}))$
34	33	cleq2lem	$⊢ t = \{\emptyset, 2_{𝑜}\} \to ((\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t)) \leftrightarrow (\{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\} \land \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})))$
35	34	adantl	$⊢ ((\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \land t = \{\emptyset, 2_{𝑜}\}) \to ((\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t)) \leftrightarrow (\{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\} \land \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})))$
36		1oex	$⊢ 1_{𝑜} \in V$
37	36	prid2	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
38		iftrue	$⊢ r = \{\emptyset\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = \{\emptyset, 1_{𝑜}\}$
39		prex	$⊢ \{\emptyset, 1_{𝑜}\} \in V$
40	38 1 39	fvmpt	$⊢ \{\emptyset\} \in 𝒫 3_{𝑜} \to K (\{\emptyset\}) = \{\emptyset, 1_{𝑜}\}$
41	40	adantr	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to K (\{\emptyset\}) = \{\emptyset, 1_{𝑜}\}$
42	37 41	eleqtrrid	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to 1_{𝑜} \in K (\{\emptyset\})$
43		1n0	$⊢ 1_{𝑜} \neq \emptyset$
44	43	neii	$⊢ \neg 1_{𝑜} = \emptyset$
45		eqcom	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow 2_{𝑜} = 1_{𝑜}$
46		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
47		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
48	46 47	eqeq12i	$⊢ 2_{𝑜} = 1_{𝑜} \leftrightarrow suc 1_{𝑜} = suc \emptyset$
49		suc11reg	$⊢ suc 1_{𝑜} = suc \emptyset \leftrightarrow 1_{𝑜} = \emptyset$
50	45 48 49	3bitri	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow 1_{𝑜} = \emptyset$
51	43 50	nemtbir	$⊢ \neg 1_{𝑜} = 2_{𝑜}$
52	44 51	pm3.2ni	$⊢ \neg (1_{𝑜} = \emptyset \lor 1_{𝑜} = 2_{𝑜})$
53		elpri	$⊢ 1_{𝑜} \in \{\emptyset, 2_{𝑜}\} \to (1_{𝑜} = \emptyset \lor 1_{𝑜} = 2_{𝑜})$
54	52 53	mto	$⊢ \neg 1_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
55	54	a1i	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg 1_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
56		eqeq1	$⊢ r = \{\emptyset, 2_{𝑜}\} \to (r = \{\emptyset\} \leftrightarrow \{\emptyset, 2_{𝑜}\} = \{\emptyset\})$
57		id	$⊢ r = \{\emptyset, 2_{𝑜}\} \to r = \{\emptyset, 2_{𝑜}\}$
58	56 57	ifbieq2d	$⊢ r = \{\emptyset, 2_{𝑜}\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (\{\emptyset, 2_{𝑜}\} = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, \{\emptyset, 2_{𝑜}\})$
59	15	prid2	$⊢ 2_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
60		2on0	$⊢ 2_{𝑜} \neq \emptyset$
61		nelsn	$⊢ 2_{𝑜} \neq \emptyset \to \neg 2_{𝑜} \in \{\emptyset\}$
62	60 61	ax-mp	$⊢ \neg 2_{𝑜} \in \{\emptyset\}$
63		nelneq2	$⊢ (2_{𝑜} \in \{\emptyset, 2_{𝑜}\} \land \neg 2_{𝑜} \in \{\emptyset\}) \to \neg \{\emptyset, 2_{𝑜}\} = \{\emptyset\}$
64	59 62 63	mp2an	$⊢ \neg \{\emptyset, 2_{𝑜}\} = \{\emptyset\}$
65	64	iffalsei	$⊢ if (\{\emptyset, 2_{𝑜}\} = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, \{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
66	58 65	eqtrdi	$⊢ r = \{\emptyset, 2_{𝑜}\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = \{\emptyset, 2_{𝑜}\}$
67		prex	$⊢ \{\emptyset, 2_{𝑜}\} \in V$
68	66 1 67	fvmpt	$⊢ \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜} \to K (\{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
69	68	adantl	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to K (\{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
70	55 69	neleqtrrd	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg 1_{𝑜} \in K (\{\emptyset, 2_{𝑜}\})$
71		nelss	$⊢ (1_{𝑜} \in K (\{\emptyset\}) \land \neg 1_{𝑜} \in K (\{\emptyset, 2_{𝑜}\})) \to \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})$
72	42 70 71	syl2anc	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})$
73		snsspr1	$⊢ \{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\}$
74	72 73	jctil	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to (\{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\} \land \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\}))$
75	30 35 74	rspcedvd	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \exists t \in 𝒫 3_{𝑜} (\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t))$
76	22 29 75	rspcedvd	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \exists s \in 𝒫 3_{𝑜} \exists t \in 𝒫 3_{𝑜} (s \subseteq t \land \neg K (s) \subseteq K (t))$
77	7 21 76	mp2an	$⊢ \exists s \in 𝒫 3_{𝑜} \exists t \in 𝒫 3_{𝑜} (s \subseteq t \land \neg K (s) \subseteq K (t))$

Metamath Proof Explorer

Theorem clsk1indlem1

Proof