Metamath Proof Explorer

Theorem clsk1independent

Description: For generalized closure functions, property K1 (isotony) is independent of the properties K0, K2, K3, K4. This contradicts a claim which appears in preprints of Table 2 in Bärbel M. R. Stadler and Peter F. Stadler. "Generalized Topological Spaces in Evolutionary Theory and Combinatorial Chemistry." J. Chem. Inf. Comput. Sci., 42:577-585, 2002. Proceedings MCC 2001, Dubrovnik. The same table row implying K1 follows from the other four appears in the supplemental materials Bärbel M. R. Stadler and Peter F. Stadler. "Basic Properties of Closure Spaces" 2001 on page 12. (Contributed by RP, 5-Jul-2021)

Ref Expression
Hypotheses clsnim.k0 
|- ( ph <-> ( k ` (/) ) = (/) )
clsnim.k1 
|- ( ps <-> A. s e. ~P b A. t e. ~P b ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) )
clsnim.k2 
|- ( ch <-> A. s e. ~P b s C_ ( k ` s ) )
clsnim.k3 
|- ( th <-> A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) )
clsnim.k4 
|- ( ta <-> A. s e. ~P b ( k ` ( k ` s ) ) = ( k ` s ) )
Assertion clsk1independent 
|- -. A. b A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps )

Proof

Step Hyp Ref Expression
1 clsnim.k0 
 |-  ( ph <-> ( k ` (/) ) = (/) )
2 clsnim.k1 
 |-  ( ps <-> A. s e. ~P b A. t e. ~P b ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) )
3 clsnim.k2 
 |-  ( ch <-> A. s e. ~P b s C_ ( k ` s ) )
4 clsnim.k3 
 |-  ( th <-> A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) )
5 clsnim.k4 
 |-  ( ta <-> A. s e. ~P b ( k ` ( k ` s ) ) = ( k ` s ) )
6 3on 
 |-  3o e. On
7 6 elexi 
 |-  3o e. _V
8 eqid 
 |-  ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) )
9 notnotr 
 |-  ( -. -. r = { (/) } -> r = { (/) } )
10 9 a1i 
 |-  ( r e. ~P 3o -> ( -. -. r = { (/) } -> r = { (/) } ) )
11 sssucid 
 |-  2o C_ suc 2o
12 2oex 
 |-  2o e. _V
13 12 elpw 
 |-  ( 2o e. ~P suc 2o <-> 2o C_ suc 2o )
14 11 13 mpbir 
 |-  2o e. ~P suc 2o
15 df2o3 
 |-  2o = { (/) , 1o }
16 df-3o 
 |-  3o = suc 2o
17 16 eqcomi 
 |-  suc 2o = 3o
18 17 pweqi 
 |-  ~P suc 2o = ~P 3o
19 14 15 18 3eltr3i 
 |-  { (/) , 1o } e. ~P 3o
20 19 2a1i 
 |-  ( r e. ~P 3o -> ( -. -. r = { (/) } -> { (/) , 1o } e. ~P 3o ) )
21 10 20 jcad 
 |-  ( r e. ~P 3o -> ( -. -. r = { (/) } -> ( r = { (/) } /\ { (/) , 1o } e. ~P 3o ) ) )
22 21 con1d 
 |-  ( r e. ~P 3o -> ( -. ( r = { (/) } /\ { (/) , 1o } e. ~P 3o ) -> -. r = { (/) } ) )
23 22 anc2ri 
 |-  ( r e. ~P 3o -> ( -. ( r = { (/) } /\ { (/) , 1o } e. ~P 3o ) -> ( -. r = { (/) } /\ r e. ~P 3o ) ) )
24 23 orrd 
 |-  ( r e. ~P 3o -> ( ( r = { (/) } /\ { (/) , 1o } e. ~P 3o ) \/ ( -. r = { (/) } /\ r e. ~P 3o ) ) )
25 ifel 
 |-  ( if ( r = { (/) } , { (/) , 1o } , r ) e. ~P 3o <-> ( ( r = { (/) } /\ { (/) , 1o } e. ~P 3o ) \/ ( -. r = { (/) } /\ r e. ~P 3o ) ) )
26 24 25 sylibr 
 |-  ( r e. ~P 3o -> if ( r = { (/) } , { (/) , 1o } , r ) e. ~P 3o )
27 8 26 fmpti 
 |-  ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) : ~P 3o --> ~P 3o
28 7 pwex 
 |-  ~P 3o e. _V
29 28 28 elmap 
 |-  ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) e. ( ~P 3o ^m ~P 3o ) <-> ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) : ~P 3o --> ~P 3o )
30 27 29 mpbir 
 |-  ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) e. ( ~P 3o ^m ~P 3o )
31 8 clsk1indlem0 
 |-  ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/)
32 8 clsk1indlem2 
 |-  A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s )
33 31 32 pm3.2i 
 |-  ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) )
34 8 clsk1indlem3 
 |-  A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) )
35 8 clsk1indlem4 
 |-  A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s )
36 34 35 pm3.2i 
 |-  ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) )
37 33 36 pm3.2i 
 |-  ( ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
38 8 clsk1indlem1 
 |-  E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) )
39 37 38 pm3.2i 
 |-  ( ( ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) /\ E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) )
40 fveq1 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( k ` (/) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) )
41 40 eqeq1d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( k ` (/) ) = (/) <-> ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) ) )
42 fveq1 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( k ` s ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) )
43 42 sseq2d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( s C_ ( k ` s ) <-> s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
44 43 ralbidv 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( A. s e. ~P 3o s C_ ( k ` s ) <-> A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
45 41 44 anbi12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) <-> ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) )
46 fveq1 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( k ` ( s u. t ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) )
47 fveq1 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( k ` t ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) )
48 42 47 uneq12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( k ` s ) u. ( k ` t ) ) = ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) )
49 46 48 sseq12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
50 49 2ralbidv 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
51 id 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) )
52 51 42 fveq12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( k ` ( k ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
53 52 42 eqeq12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( k ` ( k ` s ) ) = ( k ` s ) <-> ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
54 53 ralbidv 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) <-> A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) )
55 50 54 anbi12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) <-> ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) )
56 45 55 anbi12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) <-> ( ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) ) )
57 rexnal2 
 |-  ( E. s e. ~P 3o E. t e. ~P 3o -. ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) )
58 pm4.61 
 |-  ( -. ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> ( s C_ t /\ -. ( k ` s ) C_ ( k ` t ) ) )
59 42 47 sseq12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( k ` s ) C_ ( k ` t ) <-> ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) )
60 59 notbid 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( -. ( k ` s ) C_ ( k ` t ) <-> -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) )
61 60 anbi2d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( s C_ t /\ -. ( k ` s ) C_ ( k ` t ) ) <-> ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
62 58 61 bitrid 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( -. ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
63 62 2rexbidv 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( E. s e. ~P 3o E. t e. ~P 3o -. ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
64 57 63 bitr3id 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) )
65 56 64 anbi12d 
 |-  ( k = ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) -> ( ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) <-> ( ( ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) /\ E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) ) )
66 65 rspcev 
 |-  ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) e. ( ~P 3o ^m ~P 3o ) /\ ( ( ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( s u. t ) ) C_ ( ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) u. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) /\ A. s e. ~P 3o ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) = ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) ) ) /\ E. s e. ~P 3o E. t e. ~P 3o ( s C_ t /\ -. ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` s ) C_ ( ( r e. ~P 3o |-> if ( r = { (/) } , { (/) , 1o } , r ) ) ` t ) ) ) ) -> E. k e. ( ~P 3o ^m ~P 3o ) ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) )
67 30 39 66 mp2an 
 |-  E. k e. ( ~P 3o ^m ~P 3o ) ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) )
68 pweq 
 |-  ( b = 3o -> ~P b = ~P 3o )
69 68 68 oveq12d 
 |-  ( b = 3o -> ( ~P b ^m ~P b ) = ( ~P 3o ^m ~P 3o ) )
70 pm4.61 
 |-  ( -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) /\ -. ps ) )
71 1 a1i 
 |-  ( b = 3o -> ( ph <-> ( k ` (/) ) = (/) ) )
72 68 raleqdv 
 |-  ( b = 3o -> ( A. s e. ~P b s C_ ( k ` s ) <-> A. s e. ~P 3o s C_ ( k ` s ) ) )
73 3 72 bitrid 
 |-  ( b = 3o -> ( ch <-> A. s e. ~P 3o s C_ ( k ` s ) ) )
74 71 73 anbi12d 
 |-  ( b = 3o -> ( ( ph /\ ch ) <-> ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) ) )
75 68 raleqdv 
 |-  ( b = 3o -> ( A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) ) )
76 68 75 raleqbidv 
 |-  ( b = 3o -> ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) ) )
77 4 76 bitrid 
 |-  ( b = 3o -> ( th <-> A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) ) )
78 68 raleqdv 
 |-  ( b = 3o -> ( A. s e. ~P b ( k ` ( k ` s ) ) = ( k ` s ) <-> A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) )
79 5 78 bitrid 
 |-  ( b = 3o -> ( ta <-> A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) )
80 77 79 anbi12d 
 |-  ( b = 3o -> ( ( th /\ ta ) <-> ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) )
81 74 80 anbi12d 
 |-  ( b = 3o -> ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) <-> ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) ) )
82 68 raleqdv 
 |-  ( b = 3o -> ( A. t e. ~P b ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) )
83 68 82 raleqbidv 
 |-  ( b = 3o -> ( A. s e. ~P b A. t e. ~P b ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) <-> A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) )
84 2 83 bitrid 
 |-  ( b = 3o -> ( ps <-> A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) )
85 84 notbid 
 |-  ( b = 3o -> ( -. ps <-> -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) )
86 81 85 anbi12d 
 |-  ( b = 3o -> ( ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) /\ -. ps ) <-> ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) ) )
87 70 86 bitrid 
 |-  ( b = 3o -> ( -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) ) )
88 69 87 rexeqbidv 
 |-  ( b = 3o -> ( E. k e. ( ~P b ^m ~P b ) -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> E. k e. ( ~P 3o ^m ~P 3o ) ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) ) )
89 88 rspcev 
 |-  ( ( 3o e. _V /\ E. k e. ( ~P 3o ^m ~P 3o ) ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) ) -> E. b e. _V E. k e. ( ~P b ^m ~P b ) -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) )
90 rexnal2 
 |-  ( E. b e. _V E. k e. ( ~P b ^m ~P b ) -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> -. A. b e. _V A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) )
91 ralv 
 |-  ( A. b e. _V A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> A. b A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) )
92 90 91 xchbinx 
 |-  ( E. b e. _V E. k e. ( ~P b ^m ~P b ) -. ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) <-> -. A. b A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) )
93 89 92 sylib 
 |-  ( ( 3o e. _V /\ E. k e. ( ~P 3o ^m ~P 3o ) ( ( ( ( k ` (/) ) = (/) /\ A. s e. ~P 3o s C_ ( k ` s ) ) /\ ( A. s e. ~P 3o A. t e. ~P 3o ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ A. s e. ~P 3o ( k ` ( k ` s ) ) = ( k ` s ) ) ) /\ -. A. s e. ~P 3o A. t e. ~P 3o ( s C_ t -> ( k ` s ) C_ ( k ` t ) ) ) ) -> -. A. b A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps ) )
94 7 67 93 mp2an 
 |-  -. A. b A. k e. ( ~P b ^m ~P b ) ( ( ( ph /\ ch ) /\ ( th /\ ta ) ) -> ps )