Metamath Proof Explorer

Theorem ntrclsk3

Description: The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021)

Ref Expression
Hypotheses ntrcls.o 
|- O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
ntrcls.d 
|- D = ( O ` B )
ntrcls.r 
|- ( ph -> I D K )
Assertion ntrclsk3 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o 
 |-  O = ( i e. _V |-> ( k e. ( ~P i ^m ~P i ) |-> ( j e. ~P i |-> ( i \ ( k ` ( i \ j ) ) ) ) ) )
2 ntrcls.d 
 |-  D = ( O ` B )
3 ntrcls.r 
 |-  ( ph -> I D K )
4 fveq2 
 |-  ( s = a -> ( I ` s ) = ( I ` a ) )
5 4 ineq1d 
 |-  ( s = a -> ( ( I ` s ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` t ) ) )
6 ineq1 
 |-  ( s = a -> ( s i^i t ) = ( a i^i t ) )
7 6 fveq2d 
 |-  ( s = a -> ( I ` ( s i^i t ) ) = ( I ` ( a i^i t ) ) )
8 5 7 sseq12d 
 |-  ( s = a -> ( ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> ( ( I ` a ) i^i ( I ` t ) ) C_ ( I ` ( a i^i t ) ) ) )
9 fveq2 
 |-  ( t = b -> ( I ` t ) = ( I ` b ) )
10 9 ineq2d 
 |-  ( t = b -> ( ( I ` a ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` b ) ) )
11 ineq2 
 |-  ( t = b -> ( a i^i t ) = ( a i^i b ) )
12 11 fveq2d 
 |-  ( t = b -> ( I ` ( a i^i t ) ) = ( I ` ( a i^i b ) ) )
13 10 12 sseq12d 
 |-  ( t = b -> ( ( ( I ` a ) i^i ( I ` t ) ) C_ ( I ` ( a i^i t ) ) <-> ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) ) )
14 8 13 cbvral2vw 
 |-  ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. a e. ~P B A. b e. ~P B ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) )
15 2 3 ntrclsbex 
 |-  ( ph -> B e. _V )
16 difssd 
 |-  ( ph -> ( B \ s ) C_ B )
17 15 16 sselpwd 
 |-  ( ph -> ( B \ s ) e. ~P B )
18 17 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> ( B \ s ) e. ~P B )
19 elpwi 
 |-  ( a e. ~P B -> a C_ B )
20 simpl 
 |-  ( ( B e. _V /\ a C_ B ) -> B e. _V )
21 difssd 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ a ) C_ B )
22 20 21 sselpwd 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ a ) e. ~P B )
23 simpr 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> s = ( B \ a ) )
24 23 difeq2d 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( B \ s ) = ( B \ ( B \ a ) ) )
25 24 eqeq2d 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( a = ( B \ s ) <-> a = ( B \ ( B \ a ) ) ) )
26 eqcom 
 |-  ( a = ( B \ ( B \ a ) ) <-> ( B \ ( B \ a ) ) = a )
27 25 26 bitrdi 
 |-  ( ( ( B e. _V /\ a C_ B ) /\ s = ( B \ a ) ) -> ( a = ( B \ s ) <-> ( B \ ( B \ a ) ) = a ) )
28 dfss4 
 |-  ( a C_ B <-> ( B \ ( B \ a ) ) = a )
29 28 biimpi 
 |-  ( a C_ B -> ( B \ ( B \ a ) ) = a )
30 29 adantl 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
31 22 27 30 rspcedvd 
 |-  ( ( B e. _V /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
32 15 19 31 syl2an 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
33 simpl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ph )
34 difssd 
 |-  ( ph -> ( B \ t ) C_ B )
35 15 34 sselpwd 
 |-  ( ph -> ( B \ t ) e. ~P B )
36 33 35 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
37 elpwi 
 |-  ( b e. ~P B -> b C_ B )
38 simpl 
 |-  ( ( B e. _V /\ b C_ B ) -> B e. _V )
39 difssd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) C_ B )
40 38 39 sselpwd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) e. ~P B )
41 simpr 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> t = ( B \ b ) )
42 41 difeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
43 42 eqeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
44 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
45 43 44 bitrdi 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
46 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
47 46 biimpi 
 |-  ( b C_ B -> ( B \ ( B \ b ) ) = b )
48 47 adantl 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
49 40 45 48 rspcedvd 
 |-  ( ( B e. _V /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
50 15 37 49 syl2an 
 |-  ( ( ph /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
51 50 3ad2antl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
52 simp13 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> a = ( B \ s ) )
53 fveq2 
 |-  ( a = ( B \ s ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
54 53 ineq1d 
 |-  ( a = ( B \ s ) -> ( ( I ` a ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) )
55 ineq1 
 |-  ( a = ( B \ s ) -> ( a i^i b ) = ( ( B \ s ) i^i b ) )
56 55 fveq2d 
 |-  ( a = ( B \ s ) -> ( I ` ( a i^i b ) ) = ( I ` ( ( B \ s ) i^i b ) ) )
57 54 56 sseq12d 
 |-  ( a = ( B \ s ) -> ( ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) <-> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) C_ ( I ` ( ( B \ s ) i^i b ) ) ) )
58 52 57 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) <-> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) C_ ( I ` ( ( B \ s ) i^i b ) ) ) )
59 fveq2 
 |-  ( b = ( B \ t ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
60 59 ineq2d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) )
61 ineq2 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( ( B \ s ) i^i ( B \ t ) ) )
62 difundi 
 |-  ( B \ ( s u. t ) ) = ( ( B \ s ) i^i ( B \ t ) )
63 61 62 eqtr4di 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( B \ ( s u. t ) ) )
64 63 fveq2d 
 |-  ( b = ( B \ t ) -> ( I ` ( ( B \ s ) i^i b ) ) = ( I ` ( B \ ( s u. t ) ) ) )
65 60 64 sseq12d 
 |-  ( b = ( B \ t ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) C_ ( I ` ( ( B \ s ) i^i b ) ) <-> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ ( I ` ( B \ ( s u. t ) ) ) ) )
66 65 3ad2ant3 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) C_ ( I ` ( ( B \ s ) i^i b ) ) <-> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ ( I ` ( B \ ( s u. t ) ) ) ) )
67 simp11 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
68 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
69 68 15 jca 
 |-  ( ph -> ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) )
70 67 69 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) )
71 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
72 71 adantr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> I : ~P B --> ~P B )
73 simpr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> B e. _V )
74 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) C_ B )
75 73 74 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) e. ~P B )
76 72 75 ffvelrnd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) e. ~P B )
77 76 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) C_ B )
78 orc 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) )
79 inss 
 |-  ( ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
80 77 78 79 3syl 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
81 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) C_ B )
82 73 81 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) e. ~P B )
83 72 82 ffvelrnd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) e. ~P B )
84 83 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) C_ B )
85 80 84 jca 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B /\ ( I ` ( B \ ( s u. t ) ) ) C_ B ) )
86 sscon34b 
 |-  ( ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B /\ ( I ` ( B \ ( s u. t ) ) ) C_ B ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ ( I ` ( B \ ( s u. t ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) ) )
87 70 85 86 3syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ ( I ` ( B \ ( s u. t ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) ) )
88 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
89 88 sseq2i 
 |-  ( ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) )
90 89 a1i 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) ) )
91 67 15 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> B e. _V )
92 67 68 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I e. ( ~P B ^m ~P B ) )
93 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
94 rp-simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
95 simpl2 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
96 simpl3 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> I e. ( ~P B ^m ~P B ) )
97 eqid 
 |-  ( D ` I ) = ( D ` I )
98 simpl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
99 simprl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
100 99 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s C_ B )
101 simprr 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
102 101 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t C_ B )
103 100 102 unssd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) C_ B )
104 98 103 sselpwd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
105 104 3ad2antl2 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
106 eqid 
 |-  ( ( D ` I ) ` ( s u. t ) ) = ( ( D ` I ) ` ( s u. t ) )
107 1 2 95 96 97 105 106 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` ( s u. t ) ) = ( B \ ( I ` ( B \ ( s u. t ) ) ) ) )
108 simpl1 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ph )
109 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
110 109 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
111 108 110 syl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
112 107 111 eqtr3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) = ( K ` ( s u. t ) ) )
113 simprl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
114 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
115 1 2 95 96 97 113 114 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
116 109 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` s ) = ( K ` s ) )
117 108 116 syl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` s ) = ( K ` s ) )
118 115 117 eqtr3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( B \ ( I ` ( B \ s ) ) ) = ( K ` s ) )
119 simprr 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
120 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
121 1 2 95 96 97 119 120 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
122 109 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` t ) = ( K ` t ) )
123 108 122 syl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` t ) = ( K ` t ) )
124 121 123 eqtr3d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( B \ ( I ` ( B \ t ) ) ) = ( K ` t ) )
125 118 124 uneq12d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) = ( ( K ` s ) u. ( K ` t ) ) )
126 112 125 sseq12d 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) <-> ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
127 67 91 92 93 94 126 syl32anc 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( B \ ( I ` ( B \ ( s u. t ) ) ) ) C_ ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) <-> ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
128 87 90 127 3bitrd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ ( I ` ( B \ ( s u. t ) ) ) <-> ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
129 58 66 128 3bitrd 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) <-> ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
130 36 51 129 ralxfrd2 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) <-> A. t e. ~P B ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
131 18 32 130 ralxfrd2 
 |-  ( ph -> ( A. a e. ~P B A. b e. ~P B ( ( I ` a ) i^i ( I ` b ) ) C_ ( I ` ( a i^i b ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )
132 14 131 syl5bb 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( ( I ` s ) i^i ( I ` t ) ) C_ ( I ` ( s i^i t ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) C_ ( ( K ` s ) u. ( K ` t ) ) ) )