clsk1indlem3

Description: The ansatz closure function ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) has the K3 property of being sub-linear. (Contributed by RP, 6-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		clsk1indlem.k	$⊢ K = (r \in 𝒫 3_{𝑜} ⟼ if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r))$
2		elif	$⊢ x \in if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \leftrightarrow ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)))$
3		uneq12	$⊢ (s = \{\emptyset\} \land t = \{\emptyset\}) \to s \cup t = \{\emptyset\} \cup \{\emptyset\}$
4		unidm	$⊢ \{\emptyset\} \cup \{\emptyset\} = \{\emptyset\}$
5	3 4	eqtrdi	$⊢ (s = \{\emptyset\} \land t = \{\emptyset\}) \to s \cup t = \{\emptyset\}$
6		an3	$⊢ ((s = \{\emptyset\} \land t = \{\emptyset\}) \land (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})) \to (s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})$
7	6	orcd	$⊢ ((s = \{\emptyset\} \land t = \{\emptyset\}) \land (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s))$
8	7	orcd	$⊢ ((s = \{\emptyset\} \land t = \{\emptyset\}) \land (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
9	8	ex	$⊢ (s = \{\emptyset\} \land t = \{\emptyset\}) \to ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
10		pm2.24	$⊢ s \cup t = \{\emptyset\} \to (\neg s \cup t = \{\emptyset\} \to (x \in (s \cup t) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
11	10	impd	$⊢ s \cup t = \{\emptyset\} \to ((\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
12	9 11	jaao	$⊢ ((s = \{\emptyset\} \land t = \{\emptyset\}) \land s \cup t = \{\emptyset\}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
13	5 12	mpdan	$⊢ (s = \{\emptyset\} \land t = \{\emptyset\}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
14	13	a1i	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to ((s = \{\emptyset\} \land t = \{\emptyset\}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
15		uneqsn	$⊢ s \cup t = \{\emptyset\} \leftrightarrow ((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset) \lor (s = \emptyset \land t = \{\emptyset\}))$
16		df-3or	$⊢ ((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset) \lor (s = \emptyset \land t = \{\emptyset\})) \leftrightarrow (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset)) \lor (s = \emptyset \land t = \{\emptyset\}))$
17	15 16	bitri	$⊢ s \cup t = \{\emptyset\} \leftrightarrow (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset)) \lor (s = \emptyset \land t = \{\emptyset\}))$
18		pm2.21	$⊢ \neg s = \{\emptyset\} \to (s = \{\emptyset\} \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
19	18	adantrd	$⊢ \neg s = \{\emptyset\} \to ((s = \{\emptyset\} \land t = \{\emptyset\}) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
20	18	adantrd	$⊢ \neg s = \{\emptyset\} \to ((s = \{\emptyset\} \land t = \emptyset) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
21	19 20	jaod	$⊢ \neg s = \{\emptyset\} \to (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset)) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
22	21	adantr	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset)) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
23		pm2.21	$⊢ \neg t = \{\emptyset\} \to (t = \{\emptyset\} \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
24	23	adantl	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to (t = \{\emptyset\} \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
25	24	adantld	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \emptyset \land t = \{\emptyset\}) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
26	22 25	jaod	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (s = \{\emptyset\} \land t = \emptyset)) \lor (s = \emptyset \land t = \{\emptyset\})) \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
27	17 26	syl5bi	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to (s \cup t = \{\emptyset\} \to (x \in \{\emptyset, 1_{𝑜}\} \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
28	27	impd	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
29		elun	$⊢ x \in (s \cup t) \leftrightarrow (x \in s \lor x \in t)$
30	29	biimpi	$⊢ x \in (s \cup t) \to (x \in s \lor x \in t)$
31	30	adantl	$⊢ (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to (x \in s \lor x \in t)$
32		andi	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land (x \in s \lor x \in t)) \leftrightarrow (((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in s) \lor ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in t))$
33		simpl	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to \neg s = \{\emptyset\}$
34	33	anim1i	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in s) \to (\neg s = \{\emptyset\} \land x \in s)$
35		simpr	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to \neg t = \{\emptyset\}$
36	35	anim1i	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in t) \to (\neg t = \{\emptyset\} \land x \in t)$
37	34 36	orim12i	$⊢ (((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in s) \lor ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in t)) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (\neg t = \{\emptyset\} \land x \in t))$
38	32 37	sylbi	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land (x \in s \lor x \in t)) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (\neg t = \{\emptyset\} \land x \in t))$
39	31 38	sylan2	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (\neg t = \{\emptyset\} \land x \in t))$
40	39	olcd	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})) \lor ((\neg s = \{\emptyset\} \land x \in s) \lor (\neg t = \{\emptyset\} \land x \in t)))$
41		or4	$⊢ (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})) \lor ((\neg s = \{\emptyset\} \land x \in s) \lor (\neg t = \{\emptyset\} \land x \in t))) \leftrightarrow (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
42	40 41	sylib	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
43	42	ex	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
44	28 43	jaod	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
45	44	a1i	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
46	14 45	jaod	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\})) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
47		orc	$⊢ (s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
48	47	expcom	$⊢ x \in \{\emptyset, 1_{𝑜}\} \to (s = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
49	48	adantrd	$⊢ x \in \{\emptyset, 1_{𝑜}\} \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
50	49	adantl	$⊢ (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
51		simpr	$⊢ (x \in s \land s = \{\emptyset\}) \to s = \{\emptyset\}$
52		id	$⊢ s = \{\emptyset\} \to s = \{\emptyset\}$
53		snsspr1	$⊢ \{\emptyset\} \subseteq \{\emptyset, 1_{𝑜}\}$
54	52 53	eqsstrdi	$⊢ s = \{\emptyset\} \to s \subseteq \{\emptyset, 1_{𝑜}\}$
55	54	sseld	$⊢ s = \{\emptyset\} \to (x \in s \to x \in \{\emptyset, 1_{𝑜}\})$
56	55	impcom	$⊢ (x \in s \land s = \{\emptyset\}) \to x \in \{\emptyset, 1_{𝑜}\}$
57	51 56	jca	$⊢ (x \in s \land s = \{\emptyset\}) \to (s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})$
58	57	orcd	$⊢ (x \in s \land s = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
59	58	ex	$⊢ x \in s \to (s = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
60		olc	$⊢ (\neg t = \{\emptyset\} \land x \in t) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
61	60	expcom	$⊢ x \in t \to (\neg t = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
62	59 61	jaoa	$⊢ (x \in s \lor x \in t) \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
63	29 62	sylbi	$⊢ x \in (s \cup t) \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
64	63	adantl	$⊢ (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
65	50 64	jaoi	$⊢ ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
66		olc	$⊢ (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
67	66	expcom	$⊢ x \in \{\emptyset, 1_{𝑜}\} \to (t = \{\emptyset\} \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
68	67	adantl	$⊢ (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to (t = \{\emptyset\} \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
69	68	adantrd	$⊢ (s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
70		id	$⊢ (\neg s = \{\emptyset\} \land x \in s) \to (\neg s = \{\emptyset\} \land x \in s)$
71	70	ex	$⊢ \neg s = \{\emptyset\} \to (x \in s \to (\neg s = \{\emptyset\} \land x \in s))$
72	71	adantl	$⊢ (t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to (x \in s \to (\neg s = \{\emptyset\} \land x \in s))$
73		id	$⊢ t = \{\emptyset\} \to t = \{\emptyset\}$
74	73 53	eqsstrdi	$⊢ t = \{\emptyset\} \to t \subseteq \{\emptyset, 1_{𝑜}\}$
75	74	sseld	$⊢ t = \{\emptyset\} \to (x \in t \to x \in \{\emptyset, 1_{𝑜}\})$
76	75	anc2li	$⊢ t = \{\emptyset\} \to (x \in t \to (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
77	76	adantr	$⊢ (t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to (x \in t \to (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
78	72 77	orim12d	$⊢ (t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((x \in s \lor x \in t) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
79	78	com12	$⊢ (x \in s \lor x \in t) \to ((t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
80	29 79	sylbi	$⊢ x \in (s \cup t) \to ((t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
81	80	adantl	$⊢ (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to ((t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
82	69 81	jaoi	$⊢ ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to ((t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
83	65 82	orim12d	$⊢ ((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)) \lor ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))))$
84	83	com12	$⊢ ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)) \lor ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))))$
85		or42	$⊢ (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)) \lor ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))) \leftrightarrow (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
86	84 85	syl6ib	$⊢ ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
87	86	a1i	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))))$
88		4exmid	$⊢ (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\})) \lor ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})))$
89	88	a1i	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (((s = \{\emptyset\} \land t = \{\emptyset\}) \lor (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\})) \lor ((s = \{\emptyset\} \land \neg t = \{\emptyset\}) \lor (t = \{\emptyset\} \land \neg s = \{\emptyset\})))$
90	46 87 89	mpjaod	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (((s \cup t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t))) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
91	2 90	syl5bi	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (x \in if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \to (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))))$
92		elun	$⊢ x \in (if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \cup if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)) \leftrightarrow (x \in if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \lor x \in if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t))$
93		elif	$⊢ x \in if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \leftrightarrow ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s))$
94		elif	$⊢ x \in if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t) \leftrightarrow ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
95	93 94	orbi12i	$⊢ (x \in if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \lor x \in if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)) \leftrightarrow (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
96	92 95	sylbbr	$⊢ (((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg s = \{\emptyset\} \land x \in s)) \lor ((t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))) \to x \in (if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \cup if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t))$
97	91 96	syl6	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to (x \in if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \to x \in (if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \cup if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)))$
98	97	ssrdv	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \subseteq if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \cup if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
99		pwuncl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to s \cup t \in 𝒫 3_{𝑜}$
100		eqeq1	$⊢ r = s \cup t \to (r = \{\emptyset\} \leftrightarrow s \cup t = \{\emptyset\})$
101		id	$⊢ r = s \cup t \to r = s \cup t$
102	100 101	ifbieq2d	$⊢ r = s \cup t \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
103		prex	$⊢ \{\emptyset, 1_{𝑜}\} \in V$
104		vex	$⊢ s \in V$
105		vex	$⊢ t \in V$
106	104 105	unex	$⊢ s \cup t \in V$
107	103 106	ifex	$⊢ if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \in V$
108	102 1 107	fvmpt	$⊢ s \cup t \in 𝒫 3_{𝑜} \to K (s \cup t) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
109	99 108	syl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s \cup t) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
110		eqeq1	$⊢ r = s \to (r = \{\emptyset\} \leftrightarrow s = \{\emptyset\})$
111		id	$⊢ r = s \to r = s$
112	110 111	ifbieq2d	$⊢ r = s \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
113	103 104	ifex	$⊢ if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \in V$
114	112 1 113	fvmpt	$⊢ s \in 𝒫 3_{𝑜} \to K (s) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
115	114	adantr	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
116		eqeq1	$⊢ r = t \to (r = \{\emptyset\} \leftrightarrow t = \{\emptyset\})$
117		id	$⊢ r = t \to r = t$
118	116 117	ifbieq2d	$⊢ r = t \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
119	103 105	ifex	$⊢ if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t) \in V$
120	118 1 119	fvmpt	$⊢ t \in 𝒫 3_{𝑜} \to K (t) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
121	120	adantl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (t) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
122	115 121	uneq12d	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s) \cup K (t) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \cup if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
123	98 109 122	3sstr4d	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s \cup t) \subseteq K (s) \cup K (t)$
124	123	rgen2	$⊢ \forall s \in 𝒫 3_{𝑜} \forall t \in 𝒫 3_{𝑜} K (s \cup t) \subseteq K (s) \cup K (t)$

Metamath Proof Explorer

Theorem clsk1indlem3

Proof