Theorem 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	⊢ 𝐾 = ( 𝑟 ∈ 𝒫 3o ↦ if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) )
Assertion	clsk1indlem3	⊢ ∀ 𝑠 ∈ 𝒫 3o ∀ 𝑡 ∈ 𝒫 3o ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) )

Proof

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