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	bilani	⊢ ( ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) → ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) )
31		andi	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) ) ↔ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑠 ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑡 ) ) )
32		simpl	⊢ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ¬ 𝑠 = { ∅ } )
33	32	anim1i	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑠 ) → ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) )
34		simpr	⊢ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ¬ 𝑡 = { ∅ } )
35	34	anim1i	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑡 ) → ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) )
36	33 35	orim12i	⊢ ( ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑠 ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ 𝑥 ∈ 𝑡 ) ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
37	31 36	sylbi	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
38	30 37	sylan2	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
39	38	olcd	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
40		or4	⊢ ( ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ↔ ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
41	39 40	sylib	⊢ ( ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∧ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
42	41	ex	⊢ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) )
43	28 42	jaod	⊢ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) )
44	43	a1i	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) ) )
45	14 44	jaod	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑡 = { ∅ } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) ) )
46		orc	⊢ ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
47	46	expcom	⊢ ( 𝑥 ∈ { ∅ , 1o } → ( 𝑠 = { ∅ } → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
48	47	adantrd	⊢ ( 𝑥 ∈ { ∅ , 1o } → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
49	48	adantl	⊢ ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
50		simpr	⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 = { ∅ } ) → 𝑠 = { ∅ } )
51		id	⊢ ( 𝑠 = { ∅ } → 𝑠 = { ∅ } )
52		snsspr1	⊢ { ∅ } ⊆ { ∅ , 1o }
53	51 52	eqsstrdi	⊢ ( 𝑠 = { ∅ } → 𝑠 ⊆ { ∅ , 1o } )
54	53	sseld	⊢ ( 𝑠 = { ∅ } → ( 𝑥 ∈ 𝑠 → 𝑥 ∈ { ∅ , 1o } ) )
55	54	impcom	⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 = { ∅ } ) → 𝑥 ∈ { ∅ , 1o } )
56	50 55	jca	⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 = { ∅ } ) → ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) )
57	56	orcd	⊢ ( ( 𝑥 ∈ 𝑠 ∧ 𝑠 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
58	57	ex	⊢ ( 𝑥 ∈ 𝑠 → ( 𝑠 = { ∅ } → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
59		olc	⊢ ( ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
60	59	expcom	⊢ ( 𝑥 ∈ 𝑡 → ( ¬ 𝑡 = { ∅ } → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
61	58 60	jaoa	⊢ ( ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
62	29 61	sylbi	⊢ ( 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
63	62	adantl	⊢ ( ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
64	49 63	jaoi	⊢ ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
65		olc	⊢ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) )
66	65	expcom	⊢ ( 𝑥 ∈ { ∅ , 1o } → ( 𝑡 = { ∅ } → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
67	66	adantl	⊢ ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) → ( 𝑡 = { ∅ } → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
68	67	adantrd	⊢ ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) → ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
69		id	⊢ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) → ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) )
70	69	ex	⊢ ( ¬ 𝑠 = { ∅ } → ( 𝑥 ∈ 𝑠 → ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) )
71	70	adantl	⊢ ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( 𝑥 ∈ 𝑠 → ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) )
72		id	⊢ ( 𝑡 = { ∅ } → 𝑡 = { ∅ } )
73	72 52	eqsstrdi	⊢ ( 𝑡 = { ∅ } → 𝑡 ⊆ { ∅ , 1o } )
74	73	sseld	⊢ ( 𝑡 = { ∅ } → ( 𝑥 ∈ 𝑡 → 𝑥 ∈ { ∅ , 1o } ) )
75	74	anc2li	⊢ ( 𝑡 = { ∅ } → ( 𝑥 ∈ 𝑡 → ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) )
76	75	adantr	⊢ ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( 𝑥 ∈ 𝑡 → ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) )
77	71 76	orim12d	⊢ ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
78	77	com12	⊢ ( ( 𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡 ) → ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
79	29 78	sylbi	⊢ ( 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) → ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
80	79	adantl	⊢ ( ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) → ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
81	68 80	jaoi	⊢ ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) → ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) )
82	64 81	orim12d	⊢ ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) ) )
83	82	com12	⊢ ( ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) ) )
84		or42	⊢ ( ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ∨ ( ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ∨ ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ) ) ↔ ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
85	83 84	imbitrdi	⊢ ( ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) )
86	85	a1i	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) ) )
87		4exmid	⊢ ( ( ( 𝑠 = { ∅ } ∧ 𝑡 = { ∅ } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ) ∨ ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) )
88	87	a1i	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑡 = { ∅ } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ) ∨ ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) ) )
89	45 86 88	mpjaod	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ ( 𝑠 ∪ 𝑡 ) ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) )
90	2 89	biimtrid	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝑥 ∈ if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) → ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) ) )
91		elun	⊢ ( 𝑥 ∈ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∪ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) ↔ ( 𝑥 ∈ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∨ 𝑥 ∈ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) )
92		elif	⊢ ( 𝑥 ∈ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ↔ ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) )
93		elif	⊢ ( 𝑥 ∈ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ↔ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) )
94	92 93	orbi12i	⊢ ( ( 𝑥 ∈ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∨ 𝑥 ∈ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) ↔ ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) )
95	91 94	sylbbr	⊢ ( ( ( ( 𝑠 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑠 = { ∅ } ∧ 𝑥 ∈ 𝑠 ) ) ∨ ( ( 𝑡 = { ∅ } ∧ 𝑥 ∈ { ∅ , 1o } ) ∨ ( ¬ 𝑡 = { ∅ } ∧ 𝑥 ∈ 𝑡 ) ) ) → 𝑥 ∈ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∪ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) )
96	90 95	syl6	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝑥 ∈ if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∪ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) ) )
97	96	ssrdv	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) ⊆ ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∪ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) )
98		pwuncl	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 3o )
99		eqeq1	⊢ ( 𝑟 = ( 𝑠 ∪ 𝑡 ) → ( 𝑟 = { ∅ } ↔ ( 𝑠 ∪ 𝑡 ) = { ∅ } ) )
100		id	⊢ ( 𝑟 = ( 𝑠 ∪ 𝑡 ) → 𝑟 = ( 𝑠 ∪ 𝑡 ) )
101	99 100	ifbieq2d	⊢ ( 𝑟 = ( 𝑠 ∪ 𝑡 ) → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) )
102		prex	⊢ { ∅ , 1o } ∈ V
103		vex	⊢ 𝑠 ∈ V
104		vex	⊢ 𝑡 ∈ V
105	103 104	unex	⊢ ( 𝑠 ∪ 𝑡 ) ∈ V
106	102 105	ifex	⊢ if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) ∈ V
107	101 1 106	fvmpt	⊢ ( ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 3o → ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) )
108	98 107	syl	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) = if ( ( 𝑠 ∪ 𝑡 ) = { ∅ } , { ∅ , 1o } , ( 𝑠 ∪ 𝑡 ) ) )
109		eqeq1	⊢ ( 𝑟 = 𝑠 → ( 𝑟 = { ∅ } ↔ 𝑠 = { ∅ } ) )
110		id	⊢ ( 𝑟 = 𝑠 → 𝑟 = 𝑠 )
111	109 110	ifbieq2d	⊢ ( 𝑟 = 𝑠 → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
112	102 103	ifex	⊢ if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∈ V
113	111 1 112	fvmpt	⊢ ( 𝑠 ∈ 𝒫 3o → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
114	113	adantr	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝐾 ‘ 𝑠 ) = if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) )
115		eqeq1	⊢ ( 𝑟 = 𝑡 → ( 𝑟 = { ∅ } ↔ 𝑡 = { ∅ } ) )
116		id	⊢ ( 𝑟 = 𝑡 → 𝑟 = 𝑡 )
117	115 116	ifbieq2d	⊢ ( 𝑟 = 𝑡 → if ( 𝑟 = { ∅ } , { ∅ , 1o } , 𝑟 ) = if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) )
118	102 104	ifex	⊢ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ∈ V
119	117 1 118	fvmpt	⊢ ( 𝑡 ∈ 𝒫 3o → ( 𝐾 ‘ 𝑡 ) = if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) )
120	119	adantl	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝐾 ‘ 𝑡 ) = if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) )
121	114 120	uneq12d	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) = ( if ( 𝑠 = { ∅ } , { ∅ , 1o } , 𝑠 ) ∪ if ( 𝑡 = { ∅ } , { ∅ , 1o } , 𝑡 ) ) )
122	97 108 121	3sstr4d	⊢ ( ( 𝑠 ∈ 𝒫 3o ∧ 𝑡 ∈ 𝒫 3o ) → ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) ) )
123	122	rgen2	⊢ ∀ 𝑠 ∈ 𝒫 3o ∀ 𝑡 ∈ 𝒫 3o ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) )