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		1oelpr	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
37		iftrue	$⊢ r = \{\emptyset\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = \{\emptyset, 1_{𝑜}\}$
38		prex	$⊢ \{\emptyset, 1_{𝑜}\} \in V$
39	37 1 38	fvmpt	$⊢ \{\emptyset\} \in 𝒫 3_{𝑜} \to K (\{\emptyset\}) = \{\emptyset, 1_{𝑜}\}$
40	39	adantr	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to K (\{\emptyset\}) = \{\emptyset, 1_{𝑜}\}$
41	36 40	eleqtrrid	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to 1_{𝑜} \in K (\{\emptyset\})$
42		1n0	$⊢ 1_{𝑜} \neq \emptyset$
43	42	neii	$⊢ \neg 1_{𝑜} = \emptyset$
44		eqcom	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow 2_{𝑜} = 1_{𝑜}$
45		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
46		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
47	45 46	eqeq12i	$⊢ 2_{𝑜} = 1_{𝑜} \leftrightarrow suc 1_{𝑜} = suc \emptyset$
48		suc11reg	$⊢ suc 1_{𝑜} = suc \emptyset \leftrightarrow 1_{𝑜} = \emptyset$
49	44 47 48	3bitri	$⊢ 1_{𝑜} = 2_{𝑜} \leftrightarrow 1_{𝑜} = \emptyset$
50	42 49	nemtbir	$⊢ \neg 1_{𝑜} = 2_{𝑜}$
51	43 50	pm3.2ni	$⊢ \neg (1_{𝑜} = \emptyset \lor 1_{𝑜} = 2_{𝑜})$
52		elpri	$⊢ 1_{𝑜} \in \{\emptyset, 2_{𝑜}\} \to (1_{𝑜} = \emptyset \lor 1_{𝑜} = 2_{𝑜})$
53	51 52	mto	$⊢ \neg 1_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
54	53	a1i	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg 1_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
55		eqeq1	$⊢ r = \{\emptyset, 2_{𝑜}\} \to (r = \{\emptyset\} \leftrightarrow \{\emptyset, 2_{𝑜}\} = \{\emptyset\})$
56		id	$⊢ r = \{\emptyset, 2_{𝑜}\} \to r = \{\emptyset, 2_{𝑜}\}$
57	55 56	ifbieq2d	$⊢ r = \{\emptyset, 2_{𝑜}\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (\{\emptyset, 2_{𝑜}\} = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, \{\emptyset, 2_{𝑜}\})$
58	15	prid2	$⊢ 2_{𝑜} \in \{\emptyset, 2_{𝑜}\}$
59		2on0	$⊢ 2_{𝑜} \neq \emptyset$
60		nelsn	$⊢ 2_{𝑜} \neq \emptyset \to \neg 2_{𝑜} \in \{\emptyset\}$
61	59 60	ax-mp	$⊢ \neg 2_{𝑜} \in \{\emptyset\}$
62		nelneq2	$⊢ (2_{𝑜} \in \{\emptyset, 2_{𝑜}\} \land \neg 2_{𝑜} \in \{\emptyset\}) \to \neg \{\emptyset, 2_{𝑜}\} = \{\emptyset\}$
63	58 61 62	mp2an	$⊢ \neg \{\emptyset, 2_{𝑜}\} = \{\emptyset\}$
64	63	iffalsei	$⊢ if (\{\emptyset, 2_{𝑜}\} = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, \{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
65	57 64	eqtrdi	$⊢ r = \{\emptyset, 2_{𝑜}\} \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = \{\emptyset, 2_{𝑜}\}$
66		prex	$⊢ \{\emptyset, 2_{𝑜}\} \in V$
67	65 1 66	fvmpt	$⊢ \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜} \to K (\{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
68	67	adantl	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to K (\{\emptyset, 2_{𝑜}\}) = \{\emptyset, 2_{𝑜}\}$
69	54 68	neleqtrrd	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg 1_{𝑜} \in K (\{\emptyset, 2_{𝑜}\})$
70		nelss	$⊢ (1_{𝑜} \in K (\{\emptyset\}) \land \neg 1_{𝑜} \in K (\{\emptyset, 2_{𝑜}\})) \to \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})$
71	41 69 70	syl2anc	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\})$
72		snsspr1	$⊢ \{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\}$
73	71 72	jctil	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to (\{\emptyset\} \subseteq \{\emptyset, 2_{𝑜}\} \land \neg K (\{\emptyset\}) \subseteq K (\{\emptyset, 2_{𝑜}\}))$
74	30 35 73	rspcedvd	$⊢ (\{\emptyset\} \in 𝒫 3_{𝑜} \land \{\emptyset, 2_{𝑜}\} \in 𝒫 3_{𝑜}) \to \exists t \in 𝒫 3_{𝑜} (\{\emptyset\} \subseteq t \land \neg K (\{\emptyset\}) \subseteq K (t))$
75	22 29 74	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))$
76	7 21 75	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