Metamath Proof Explorer

Theorem clsk3nimkb

Description: If the base set is not empty, axiom K3 does not imply KB. A concrete example with a pseudo-closure function of k = ( x e. ~P b |-> ( b \ x ) ) is given. (Contributed by RP, 16-Jun-2021)

Ref Expression
Assertion clsk3nimkb 
|- -. A. b A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) )

Proof

Step Hyp Ref Expression
1 1oex 
 |-  1o e. _V
2 1n0 
 |-  1o =/= (/)
3 nelsn 
 |-  ( 1o =/= (/) -> -. 1o e. { (/) } )
4 2 3 ax-mp 
 |-  -. 1o e. { (/) }
5 eldif 
 |-  ( 1o e. ( _V \ { (/) } ) <-> ( 1o e. _V /\ -. 1o e. { (/) } ) )
6 ne0i 
 |-  ( 1o e. ( _V \ { (/) } ) -> ( _V \ { (/) } ) =/= (/) )
7 5 6 sylbir 
 |-  ( ( 1o e. _V /\ -. 1o e. { (/) } ) -> ( _V \ { (/) } ) =/= (/) )
8 1 4 7 mp2an 
 |-  ( _V \ { (/) } ) =/= (/)
9 r19.2zb 
 |-  ( ( _V \ { (/) } ) =/= (/) <-> ( A. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) -> E. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) ) )
10 8 9 mpbi 
 |-  ( A. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) -> E. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
11 rexex 
 |-  ( E. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) -> E. b E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
12 rexanali 
 |-  ( E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) <-> -. A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
13 12 exbii 
 |-  ( E. b E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) <-> E. b -. A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
14 exnal 
 |-  ( E. b -. A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) <-> -. A. b A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
15 13 14 sylbb 
 |-  ( E. b E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) -> -. A. b A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
16 10 11 15 3syl 
 |-  ( A. b e. ( _V \ { (/) } ) E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) -> -. A. b A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
17 difelpw 
 |-  ( b e. ( _V \ { (/) } ) -> ( b \ x ) e. ~P b )
18 17 adantr 
 |-  ( ( b e. ( _V \ { (/) } ) /\ x e. ~P b ) -> ( b \ x ) e. ~P b )
19 18 fmpttd 
 |-  ( b e. ( _V \ { (/) } ) -> ( x e. ~P b |-> ( b \ x ) ) : ~P b --> ~P b )
20 pwexg 
 |-  ( b e. ( _V \ { (/) } ) -> ~P b e. _V )
21 20 20 elmapd 
 |-  ( b e. ( _V \ { (/) } ) -> ( ( x e. ~P b |-> ( b \ x ) ) e. ( ~P b ^m ~P b ) <-> ( x e. ~P b |-> ( b \ x ) ) : ~P b --> ~P b ) )
22 19 21 mpbird 
 |-  ( b e. ( _V \ { (/) } ) -> ( x e. ~P b |-> ( b \ x ) ) e. ( ~P b ^m ~P b ) )
23 simpllr 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> k = ( x e. ~P b |-> ( b \ x ) ) )
24 difeq2 
 |-  ( x = z -> ( b \ x ) = ( b \ z ) )
25 24 cbvmptv 
 |-  ( x e. ~P b |-> ( b \ x ) ) = ( z e. ~P b |-> ( b \ z ) )
26 23 25 eqtrdi 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> k = ( z e. ~P b |-> ( b \ z ) ) )
27 difeq2 
 |-  ( z = ( s u. t ) -> ( b \ z ) = ( b \ ( s u. t ) ) )
28 27 adantl 
 |-  ( ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) /\ z = ( s u. t ) ) -> ( b \ z ) = ( b \ ( s u. t ) ) )
29 simplll 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> b e. ( _V \ { (/) } ) )
30 simplr 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> s e. ~P b )
31 30 elpwid 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> s C_ b )
32 simpr 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> t e. ~P b )
33 32 elpwid 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> t C_ b )
34 31 33 unssd 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( s u. t ) C_ b )
35 29 34 sselpwd 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( s u. t ) e. ~P b )
36 vex 
 |-  b e. _V
37 36 difexi 
 |-  ( b \ ( s u. t ) ) e. _V
38 37 a1i 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( b \ ( s u. t ) ) e. _V )
39 26 28 35 38 fvmptd 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( k ` ( s u. t ) ) = ( b \ ( s u. t ) ) )
40 difeq2 
 |-  ( z = s -> ( b \ z ) = ( b \ s ) )
41 40 adantl 
 |-  ( ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) /\ z = s ) -> ( b \ z ) = ( b \ s ) )
42 36 difexi 
 |-  ( b \ s ) e. _V
43 42 a1i 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( b \ s ) e. _V )
44 26 41 30 43 fvmptd 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( k ` s ) = ( b \ s ) )
45 difeq2 
 |-  ( z = t -> ( b \ z ) = ( b \ t ) )
46 45 adantl 
 |-  ( ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) /\ z = t ) -> ( b \ z ) = ( b \ t ) )
47 36 difexi 
 |-  ( b \ t ) e. _V
48 47 a1i 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( b \ t ) e. _V )
49 26 46 32 48 fvmptd 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( k ` t ) = ( b \ t ) )
50 44 49 uneq12d 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( ( k ` s ) u. ( k ` t ) ) = ( ( b \ s ) u. ( b \ t ) ) )
51 difindi 
 |-  ( b \ ( s i^i t ) ) = ( ( b \ s ) u. ( b \ t ) )
52 50 51 eqtr4di 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( ( k ` s ) u. ( k ` t ) ) = ( b \ ( s i^i t ) ) )
53 39 52 sseq12d 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) ) )
54 53 ralbidva 
 |-  ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) -> ( A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> A. t e. ~P b ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) ) )
55 54 ralbidva 
 |-  ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) -> ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) <-> A. s e. ~P b A. t e. ~P b ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) ) )
56 52 eqeq1d 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( ( ( k ` s ) u. ( k ` t ) ) = b <-> ( b \ ( s i^i t ) ) = b ) )
57 56 imbi2d 
 |-  ( ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) /\ t e. ~P b ) -> ( ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) <-> ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) )
58 57 ralbidva 
 |-  ( ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) /\ s e. ~P b ) -> ( A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) <-> A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) )
59 58 ralbidva 
 |-  ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) -> ( A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) <-> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) )
60 59 notbid 
 |-  ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) -> ( -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) <-> -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) )
61 55 60 anbi12d 
 |-  ( ( b e. ( _V \ { (/) } ) /\ k = ( x e. ~P b |-> ( b \ x ) ) ) -> ( ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) <-> ( A. s e. ~P b A. t e. ~P b ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) ) )
62 pwidg 
 |-  ( b e. ( _V \ { (/) } ) -> b e. ~P b )
63 ssidd 
 |-  ( b e. ( _V \ { (/) } ) -> b C_ b )
64 eldifsnneq 
 |-  ( b e. ( _V \ { (/) } ) -> -. b = (/) )
65 uneq1 
 |-  ( s = b -> ( s u. t ) = ( b u. t ) )
66 65 eqeq1d 
 |-  ( s = b -> ( ( s u. t ) = b <-> ( b u. t ) = b ) )
67 ssequn2 
 |-  ( t C_ b <-> ( b u. t ) = b )
68 66 67 bitr4di 
 |-  ( s = b -> ( ( s u. t ) = b <-> t C_ b ) )
69 ineq1 
 |-  ( s = b -> ( s i^i t ) = ( b i^i t ) )
70 69 difeq2d 
 |-  ( s = b -> ( b \ ( s i^i t ) ) = ( b \ ( b i^i t ) ) )
71 70 eqeq1d 
 |-  ( s = b -> ( ( b \ ( s i^i t ) ) = b <-> ( b \ ( b i^i t ) ) = b ) )
72 71 notbid 
 |-  ( s = b -> ( -. ( b \ ( s i^i t ) ) = b <-> -. ( b \ ( b i^i t ) ) = b ) )
73 68 72 anbi12d 
 |-  ( s = b -> ( ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) <-> ( t C_ b /\ -. ( b \ ( b i^i t ) ) = b ) ) )
74 sseq1 
 |-  ( t = b -> ( t C_ b <-> b C_ b ) )
75 ineq2 
 |-  ( t = b -> ( b i^i t ) = ( b i^i b ) )
76 inidm 
 |-  ( b i^i b ) = b
77 75 76 eqtrdi 
 |-  ( t = b -> ( b i^i t ) = b )
78 77 difeq2d 
 |-  ( t = b -> ( b \ ( b i^i t ) ) = ( b \ b ) )
79 difid 
 |-  ( b \ b ) = (/)
80 78 79 eqtrdi 
 |-  ( t = b -> ( b \ ( b i^i t ) ) = (/) )
81 80 eqeq1d 
 |-  ( t = b -> ( ( b \ ( b i^i t ) ) = b <-> (/) = b ) )
82 eqcom 
 |-  ( (/) = b <-> b = (/) )
83 81 82 bitrdi 
 |-  ( t = b -> ( ( b \ ( b i^i t ) ) = b <-> b = (/) ) )
84 83 notbid 
 |-  ( t = b -> ( -. ( b \ ( b i^i t ) ) = b <-> -. b = (/) ) )
85 74 84 anbi12d 
 |-  ( t = b -> ( ( t C_ b /\ -. ( b \ ( b i^i t ) ) = b ) <-> ( b C_ b /\ -. b = (/) ) ) )
86 73 85 rspc2ev 
 |-  ( ( b e. ~P b /\ b e. ~P b /\ ( b C_ b /\ -. b = (/) ) ) -> E. s e. ~P b E. t e. ~P b ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) )
87 62 62 63 64 86 syl112anc 
 |-  ( b e. ( _V \ { (/) } ) -> E. s e. ~P b E. t e. ~P b ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) )
88 rexanali 
 |-  ( E. t e. ~P b ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) <-> -. A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) )
89 88 rexbii 
 |-  ( E. s e. ~P b E. t e. ~P b ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) <-> E. s e. ~P b -. A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) )
90 rexnal 
 |-  ( E. s e. ~P b -. A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) <-> -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) )
91 89 90 sylbb 
 |-  ( E. s e. ~P b E. t e. ~P b ( ( s u. t ) = b /\ -. ( b \ ( s i^i t ) ) = b ) -> -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) )
92 87 91 syl 
 |-  ( b e. ( _V \ { (/) } ) -> -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) )
93 inss1 
 |-  ( s i^i t ) C_ s
94 ssun1 
 |-  s C_ ( s u. t )
95 93 94 sstri 
 |-  ( s i^i t ) C_ ( s u. t )
96 sscon 
 |-  ( ( s i^i t ) C_ ( s u. t ) -> ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) )
97 95 96 ax-mp 
 |-  ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) )
98 97 rgen2w 
 |-  A. s e. ~P b A. t e. ~P b ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) )
99 92 98 jctil 
 |-  ( b e. ( _V \ { (/) } ) -> ( A. s e. ~P b A. t e. ~P b ( b \ ( s u. t ) ) C_ ( b \ ( s i^i t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( b \ ( s i^i t ) ) = b ) ) )
100 22 61 99 rspcedvd 
 |-  ( b e. ( _V \ { (/) } ) -> E. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) /\ -. A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) ) )
101 16 100 mprg 
 |-  -. A. b A. k e. ( ~P b ^m ~P b ) ( A. s e. ~P b A. t e. ~P b ( k ` ( s u. t ) ) C_ ( ( k ` s ) u. ( k ` t ) ) -> A. s e. ~P b A. t e. ~P b ( ( s u. t ) = b -> ( ( k ` s ) u. ( k ` t ) ) = b ) )