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 bilani 
 |-  ( ( -. ( s u. t ) = { (/) } /\ x e. ( s u. t ) ) -> ( x e. s \/ x e. t ) )
31 andi 
 |-  ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ ( x e. s \/ x e. t ) ) <-> ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. s ) \/ ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. t ) ) )
32 simpl 
 |-  ( ( -. s = { (/) } /\ -. t = { (/) } ) -> -. s = { (/) } )
33 32 anim1i 
 |-  ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. s ) -> ( -. s = { (/) } /\ x e. s ) )
34 simpr 
 |-  ( ( -. s = { (/) } /\ -. t = { (/) } ) -> -. t = { (/) } )
35 34 anim1i 
 |-  ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. t ) -> ( -. t = { (/) } /\ x e. t ) )
36 33 35 orim12i 
 |-  ( ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. s ) \/ ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ x e. t ) ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( -. t = { (/) } /\ x e. t ) ) )
37 31 36 sylbi 
 |-  ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ ( x e. s \/ x e. t ) ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( -. t = { (/) } /\ x e. t ) ) )
38 30 37 sylan2 
 |-  ( ( ( -. s = { (/) } /\ -. t = { (/) } ) /\ ( -. ( s u. t ) = { (/) } /\ x e. ( s u. t ) ) ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( -. t = { (/) } /\ x e. t ) ) )
39 38 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 ) ) ) )
40 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 ) ) ) )
41 39 40 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 ) ) ) )
42 41 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 ) ) ) ) )
43 28 42 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 ) ) ) ) )
44 43 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 ) ) ) ) ) )
45 14 44 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 ) ) ) ) ) )
46 orc 
 |-  ( ( s = { (/) } /\ x e. { (/) , 1o } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) )
47 46 expcom 
 |-  ( x e. { (/) , 1o } -> ( s = { (/) } -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
48 47 adantrd 
 |-  ( x e. { (/) , 1o } -> ( ( s = { (/) } /\ -. t = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
49 48 adantl 
 |-  ( ( ( s u. t ) = { (/) } /\ x e. { (/) , 1o } ) -> ( ( s = { (/) } /\ -. t = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
50 simpr 
 |-  ( ( x e. s /\ s = { (/) } ) -> s = { (/) } )
51 id 
 |-  ( s = { (/) } -> s = { (/) } )
52 snsspr1 
 |-  { (/) } C_ { (/) , 1o }
53 51 52 eqsstrdi 
 |-  ( s = { (/) } -> s C_ { (/) , 1o } )
54 53 sseld 
 |-  ( s = { (/) } -> ( x e. s -> x e. { (/) , 1o } ) )
55 54 impcom 
 |-  ( ( x e. s /\ s = { (/) } ) -> x e. { (/) , 1o } )
56 50 55 jca 
 |-  ( ( x e. s /\ s = { (/) } ) -> ( s = { (/) } /\ x e. { (/) , 1o } ) )
57 56 orcd 
 |-  ( ( x e. s /\ s = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) )
58 57 ex 
 |-  ( x e. s -> ( s = { (/) } -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
59 olc 
 |-  ( ( -. t = { (/) } /\ x e. t ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) )
60 59 expcom 
 |-  ( x e. t -> ( -. t = { (/) } -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
61 58 60 jaoa 
 |-  ( ( x e. s \/ x e. t ) -> ( ( s = { (/) } /\ -. t = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
62 29 61 sylbi 
 |-  ( x e. ( s u. t ) -> ( ( s = { (/) } /\ -. t = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
63 62 adantl 
 |-  ( ( -. ( s u. t ) = { (/) } /\ x e. ( s u. t ) ) -> ( ( s = { (/) } /\ -. t = { (/) } ) -> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) ) )
64 49 63 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 ) ) ) )
65 olc 
 |-  ( ( t = { (/) } /\ x e. { (/) , 1o } ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) )
66 65 expcom 
 |-  ( x e. { (/) , 1o } -> ( t = { (/) } -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
67 66 adantl 
 |-  ( ( ( s u. t ) = { (/) } /\ x e. { (/) , 1o } ) -> ( t = { (/) } -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
68 67 adantrd 
 |-  ( ( ( s u. t ) = { (/) } /\ x e. { (/) , 1o } ) -> ( ( t = { (/) } /\ -. s = { (/) } ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
69 id 
 |-  ( ( -. s = { (/) } /\ x e. s ) -> ( -. s = { (/) } /\ x e. s ) )
70 69 ex 
 |-  ( -. s = { (/) } -> ( x e. s -> ( -. s = { (/) } /\ x e. s ) ) )
71 70 adantl 
 |-  ( ( t = { (/) } /\ -. s = { (/) } ) -> ( x e. s -> ( -. s = { (/) } /\ x e. s ) ) )
72 id 
 |-  ( t = { (/) } -> t = { (/) } )
73 72 52 eqsstrdi 
 |-  ( t = { (/) } -> t C_ { (/) , 1o } )
74 73 sseld 
 |-  ( t = { (/) } -> ( x e. t -> x e. { (/) , 1o } ) )
75 74 anc2li 
 |-  ( t = { (/) } -> ( x e. t -> ( t = { (/) } /\ x e. { (/) , 1o } ) ) )
76 75 adantr 
 |-  ( ( t = { (/) } /\ -. s = { (/) } ) -> ( x e. t -> ( t = { (/) } /\ x e. { (/) , 1o } ) ) )
77 71 76 orim12d 
 |-  ( ( t = { (/) } /\ -. s = { (/) } ) -> ( ( x e. s \/ x e. t ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
78 77 com12 
 |-  ( ( x e. s \/ x e. t ) -> ( ( t = { (/) } /\ -. s = { (/) } ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
79 29 78 sylbi 
 |-  ( x e. ( s u. t ) -> ( ( t = { (/) } /\ -. s = { (/) } ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
80 79 adantl 
 |-  ( ( -. ( s u. t ) = { (/) } /\ x e. ( s u. t ) ) -> ( ( t = { (/) } /\ -. s = { (/) } ) -> ( ( -. s = { (/) } /\ x e. s ) \/ ( t = { (/) } /\ x e. { (/) , 1o } ) ) ) )
81 68 80 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 } ) ) ) )
82 64 81 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 } ) ) ) ) )
83 82 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 } ) ) ) ) )
84 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 ) ) ) )
85 83 84 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 ) ) ) ) )
86 85 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 ) ) ) ) ) )
87 4exmid 
 |-  ( ( ( s = { (/) } /\ t = { (/) } ) \/ ( -. s = { (/) } /\ -. t = { (/) } ) ) \/ ( ( s = { (/) } /\ -. t = { (/) } ) \/ ( t = { (/) } /\ -. s = { (/) } ) ) )
88 87 a1i 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( ( ( s = { (/) } /\ t = { (/) } ) \/ ( -. s = { (/) } /\ -. t = { (/) } ) ) \/ ( ( s = { (/) } /\ -. t = { (/) } ) \/ ( t = { (/) } /\ -. s = { (/) } ) ) ) )
89 45 86 88 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 ) ) ) ) )
90 2 89 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 ) ) ) ) )
91 elun 
 |-  ( x e. ( if ( s = { (/) } , { (/) , 1o } , s ) u. if ( t = { (/) } , { (/) , 1o } , t ) ) <-> ( x e. if ( s = { (/) } , { (/) , 1o } , s ) \/ x e. if ( t = { (/) } , { (/) , 1o } , t ) ) )
92 elif 
 |-  ( x e. if ( s = { (/) } , { (/) , 1o } , s ) <-> ( ( s = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. s = { (/) } /\ x e. s ) ) )
93 elif 
 |-  ( x e. if ( t = { (/) } , { (/) , 1o } , t ) <-> ( ( t = { (/) } /\ x e. { (/) , 1o } ) \/ ( -. t = { (/) } /\ x e. t ) ) )
94 92 93 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 ) ) ) )
95 91 94 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 ) ) )
96 90 95 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 ) ) ) )
97 96 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 ) ) )
98 pwuncl 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( s u. t ) e. ~P 3o )
99 eqeq1 
 |-  ( r = ( s u. t ) -> ( r = { (/) } <-> ( s u. t ) = { (/) } ) )
100 id 
 |-  ( r = ( s u. t ) -> r = ( s u. t ) )
101 99 100 ifbieq2d 
 |-  ( r = ( s u. t ) -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( ( s u. t ) = { (/) } , { (/) , 1o } , ( s u. t ) ) )
102 prex 
 |-  { (/) , 1o } e. _V
103 vex 
 |-  s e. _V
104 vex 
 |-  t e. _V
105 103 104 unex 
 |-  ( s u. t ) e. _V
106 102 105 ifex 
 |-  if ( ( s u. t ) = { (/) } , { (/) , 1o } , ( s u. t ) ) e. _V
107 101 1 106 fvmpt 
 |-  ( ( s u. t ) e. ~P 3o -> ( K ` ( s u. t ) ) = if ( ( s u. t ) = { (/) } , { (/) , 1o } , ( s u. t ) ) )
108 98 107 syl 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( K ` ( s u. t ) ) = if ( ( s u. t ) = { (/) } , { (/) , 1o } , ( s u. t ) ) )
109 eqeq1 
 |-  ( r = s -> ( r = { (/) } <-> s = { (/) } ) )
110 id 
 |-  ( r = s -> r = s )
111 109 110 ifbieq2d 
 |-  ( r = s -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( s = { (/) } , { (/) , 1o } , s ) )
112 102 103 ifex 
 |-  if ( s = { (/) } , { (/) , 1o } , s ) e. _V
113 111 1 112 fvmpt 
 |-  ( s e. ~P 3o -> ( K ` s ) = if ( s = { (/) } , { (/) , 1o } , s ) )
114 113 adantr 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( K ` s ) = if ( s = { (/) } , { (/) , 1o } , s ) )
115 eqeq1 
 |-  ( r = t -> ( r = { (/) } <-> t = { (/) } ) )
116 id 
 |-  ( r = t -> r = t )
117 115 116 ifbieq2d 
 |-  ( r = t -> if ( r = { (/) } , { (/) , 1o } , r ) = if ( t = { (/) } , { (/) , 1o } , t ) )
118 102 104 ifex 
 |-  if ( t = { (/) } , { (/) , 1o } , t ) e. _V
119 117 1 118 fvmpt 
 |-  ( t e. ~P 3o -> ( K ` t ) = if ( t = { (/) } , { (/) , 1o } , t ) )
120 119 adantl 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( K ` t ) = if ( t = { (/) } , { (/) , 1o } , t ) )
121 114 120 uneq12d 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( ( K ` s ) u. ( K ` t ) ) = ( if ( s = { (/) } , { (/) , 1o } , s ) u. if ( t = { (/) } , { (/) , 1o } , t ) ) )
122 97 108 121 3sstr4d 
 |-  ( ( s e. ~P 3o /\ t e. ~P 3o ) -> ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) )
123 122 rgen2 
 |-  A. s e. ~P 3o A. t e. ~P 3o ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) )