Metamath Proof Explorer

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 syl5bi ⊢ ( ( ¬ 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) → ( ( 𝑠 ∪ 𝑡 ) = { ∅ } → ( 𝑥 ∈ { ∅ , 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 syl6ib ⊢ ( ( ( 𝑠 = { ∅ } ∧ ¬ 𝑡 = { ∅ } ) ∨ ( 𝑡 = { ∅ } ∧ ¬ 𝑠 = { ∅ } ) ) → ( ( ( ( 𝑠 ∪ 𝑡 ) = { ∅ } ∧ 𝑥 ∈ { ∅ , 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 syl5bi ⊢ ( ( 𝑠 ∈ 𝒫 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 ( 𝐾 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐾 ‘ 𝑠 ) ∪ ( 𝐾 ‘ 𝑡 ) )