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	biimtrid	$⊢ (\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	bilani	$⊢ (\neg s \cup t = \{\emptyset\} \land x \in (s \cup t)) \to (x \in s \lor x \in t)$
31		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))$
32		simpl	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to \neg s = \{\emptyset\}$
33	32	anim1i	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in s) \to (\neg s = \{\emptyset\} \land x \in s)$
34		simpr	$⊢ (\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \to \neg t = \{\emptyset\}$
35	34	anim1i	$⊢ ((\neg s = \{\emptyset\} \land \neg t = \{\emptyset\}) \land x \in t) \to (\neg t = \{\emptyset\} \land x \in t)$
36	33 35	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))$
37	31 36	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))$
38	30 37	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))$
39	38	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)))$
40		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)))$
41	39 40	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)))$
42	41	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))))$
43	28 42	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))))$
44	43	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)))))$
45	14 44	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)))))$
46		orc	$⊢ (s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
47	46	expcom	$⊢ x \in \{\emptyset, 1_{𝑜}\} \to (s = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
48	47	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)))$
49	48	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)))$
50		simpr	$⊢ (x \in s \land s = \{\emptyset\}) \to s = \{\emptyset\}$
51		id	$⊢ s = \{\emptyset\} \to s = \{\emptyset\}$
52		snsspr1	$⊢ \{\emptyset\} \subseteq \{\emptyset, 1_{𝑜}\}$
53	51 52	eqsstrdi	$⊢ s = \{\emptyset\} \to s \subseteq \{\emptyset, 1_{𝑜}\}$
54	53	sseld	$⊢ s = \{\emptyset\} \to (x \in s \to x \in \{\emptyset, 1_{𝑜}\})$
55	54	impcom	$⊢ (x \in s \land s = \{\emptyset\}) \to x \in \{\emptyset, 1_{𝑜}\}$
56	50 55	jca	$⊢ (x \in s \land s = \{\emptyset\}) \to (s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})$
57	56	orcd	$⊢ (x \in s \land s = \{\emptyset\}) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
58	57	ex	$⊢ x \in s \to (s = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
59		olc	$⊢ (\neg t = \{\emptyset\} \land x \in t) \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t))$
60	59	expcom	$⊢ x \in t \to (\neg t = \{\emptyset\} \to ((s = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \lor (\neg t = \{\emptyset\} \land x \in t)))$
61	58 60	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)))$
62	29 61	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)))$
63	62	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)))$
64	49 63	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)))$
65		olc	$⊢ (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}) \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
66	65	expcom	$⊢ x \in \{\emptyset, 1_{𝑜}\} \to (t = \{\emptyset\} \to ((\neg s = \{\emptyset\} \land x \in s) \lor (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\})))$
67	66	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_{𝑜}\})))$
68	67	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_{𝑜}\})))$
69		id	$⊢ (\neg s = \{\emptyset\} \land x \in s) \to (\neg s = \{\emptyset\} \land x \in s)$
70	69	ex	$⊢ \neg s = \{\emptyset\} \to (x \in s \to (\neg s = \{\emptyset\} \land x \in s))$
71	70	adantl	$⊢ (t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to (x \in s \to (\neg s = \{\emptyset\} \land x \in s))$
72		id	$⊢ t = \{\emptyset\} \to t = \{\emptyset\}$
73	72 52	eqsstrdi	$⊢ t = \{\emptyset\} \to t \subseteq \{\emptyset, 1_{𝑜}\}$
74	73	sseld	$⊢ t = \{\emptyset\} \to (x \in t \to x \in \{\emptyset, 1_{𝑜}\})$
75	74	anc2li	$⊢ t = \{\emptyset\} \to (x \in t \to (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
76	75	adantr	$⊢ (t = \{\emptyset\} \land \neg s = \{\emptyset\}) \to (x \in t \to (t = \{\emptyset\} \land x \in \{\emptyset, 1_{𝑜}\}))$
77	71 76	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_{𝑜}\})))$
78	77	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_{𝑜}\})))$
79	29 78	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_{𝑜}\})))$
80	79	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_{𝑜}\})))$
81	68 80	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_{𝑜}\})))$
82	64 81	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_{𝑜}\}))))$
83	82	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_{𝑜}\}))))$
84		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)))$
85	83 84	imbitrdi	$⊢ ((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))))$
86	85	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)))))$
87		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\})))$
88	87	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\})))$
89	45 86 88	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))))$
90	2 89	biimtrid	$⊢ (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))))$
91		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))$
92		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))$
93		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))$
94	92 93	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)))$
95	91 94	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))$
96	90 95	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)))$
97	96	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)$
98		pwuncl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to s \cup t \in 𝒫 3_{𝑜}$
99		eqeq1	$⊢ r = s \cup t \to (r = \{\emptyset\} \leftrightarrow s \cup t = \{\emptyset\})$
100		id	$⊢ r = s \cup t \to r = s \cup t$
101	99 100	ifbieq2d	$⊢ r = s \cup t \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
102		prex	$⊢ \{\emptyset, 1_{𝑜}\} \in V$
103		vex	$⊢ s \in V$
104		vex	$⊢ t \in V$
105	103 104	unex	$⊢ s \cup t \in V$
106	102 105	ifex	$⊢ if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t) \in V$
107	101 1 106	fvmpt	$⊢ s \cup t \in 𝒫 3_{𝑜} \to K (s \cup t) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
108	98 107	syl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s \cup t) = if (s \cup t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s \cup t)$
109		eqeq1	$⊢ r = s \to (r = \{\emptyset\} \leftrightarrow s = \{\emptyset\})$
110		id	$⊢ r = s \to r = s$
111	109 110	ifbieq2d	$⊢ r = s \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
112	102 103	ifex	$⊢ if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s) \in V$
113	111 1 112	fvmpt	$⊢ s \in 𝒫 3_{𝑜} \to K (s) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
114	113	adantr	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s) = if (s = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, s)$
115		eqeq1	$⊢ r = t \to (r = \{\emptyset\} \leftrightarrow t = \{\emptyset\})$
116		id	$⊢ r = t \to r = t$
117	115 116	ifbieq2d	$⊢ r = t \to if (r = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, r) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
118	102 104	ifex	$⊢ if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t) \in V$
119	117 1 118	fvmpt	$⊢ t \in 𝒫 3_{𝑜} \to K (t) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
120	119	adantl	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (t) = if (t = \{\emptyset\}, \{\emptyset, 1_{𝑜}\}, t)$
121	114 120	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)$
122	97 108 121	3sstr4d	$⊢ (s \in 𝒫 3_{𝑜} \land t \in 𝒫 3_{𝑜}) \to K (s \cup t) \subseteq K (s) \cup K (t)$
123	122	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