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 
|- K = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
Assertion clsk1indlem3 
|- A. s e. ~P 3o A. t e. ~P 3o ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) )

Proof

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