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 bilani 
 |-  ( ( B e. _V /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
30 22 27 29 rspcedvd 
 |-  ( ( B e. _V /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
31 15 19 30 syl2an 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
32 simpl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ph )
33 difssd 
 |-  ( ph -> ( B \ t ) C_ B )
34 15 33 sselpwd 
 |-  ( ph -> ( B \ t ) e. ~P B )
35 32 34 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
36 elpwi 
 |-  ( b e. ~P B -> b C_ B )
37 simpl 
 |-  ( ( B e. _V /\ b C_ B ) -> B e. _V )
38 difssd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) C_ B )
39 37 38 sselpwd 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ b ) e. ~P B )
40 simpr 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> t = ( B \ b ) )
41 40 difeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
42 41 eqeq2d 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
43 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
44 42 43 bitrdi 
 |-  ( ( ( B e. _V /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
45 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
46 45 bilani 
 |-  ( ( B e. _V /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
47 39 44 46 rspcedvd 
 |-  ( ( B e. _V /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
48 15 36 47 syl2an 
 |-  ( ( ph /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
49 48 3ad2antl1 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
50 simp13 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> a = ( B \ s ) )
51 fveq2 
 |-  ( a = ( B \ s ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
52 51 ineq1d 
 |-  ( a = ( B \ s ) -> ( ( I ` a ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) )
53 ineq1 
 |-  ( a = ( B \ s ) -> ( a i^i b ) = ( ( B \ s ) i^i b ) )
54 53 fveq2d 
 |-  ( a = ( B \ s ) -> ( I ` ( a i^i b ) ) = ( I ` ( ( B \ s ) i^i b ) ) )
55 52 54 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 ) ) ) )
56 50 55 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 ) ) ) )
57 fveq2 
 |-  ( b = ( B \ t ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
58 57 ineq2d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) )
59 ineq2 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( ( B \ s ) i^i ( B \ t ) ) )
60 difundi 
 |-  ( B \ ( s u. t ) ) = ( ( B \ s ) i^i ( B \ t ) )
61 59 60 eqtr4di 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( B \ ( s u. t ) ) )
62 61 fveq2d 
 |-  ( b = ( B \ t ) -> ( I ` ( ( B \ s ) i^i b ) ) = ( I ` ( B \ ( s u. t ) ) ) )
63 58 62 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 ) ) ) ) )
64 63 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 ) ) ) ) )
65 simp11 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
66 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
67 66 15 jca 
 |-  ( ph -> ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) )
68 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
69 68 adantr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> I : ~P B --> ~P B )
70 simpr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> B e. _V )
71 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) C_ B )
72 70 71 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) e. ~P B )
73 69 72 ffvelcdmd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) e. ~P B )
74 73 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) C_ B )
75 orc 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) )
76 inss 
 |-  ( ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
77 74 75 76 3syl 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
78 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) C_ B )
79 70 78 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) e. ~P B )
80 69 79 ffvelcdmd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) e. ~P B )
81 80 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) C_ B )
82 77 81 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 ) )
83 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 ) ) ) ) ) )
84 65 67 82 83 4syl 
 |-  ( ( ( 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 ) ) ) ) ) )
85 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
86 85 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 ) ) ) ) )
87 86 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 ) ) ) ) ) )
88 65 15 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> B e. _V )
89 65 66 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> I e. ( ~P B ^m ~P B ) )
90 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
91 rp-simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
92 simpl2 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
93 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 ) )
94 eqid 
 |-  ( D ` I ) = ( D ` I )
95 simpl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
96 simprl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
97 96 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s C_ B )
98 simprr 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
99 98 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t C_ B )
100 97 99 unssd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) C_ B )
101 95 100 sselpwd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
102 101 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 )
103 eqid 
 |-  ( ( D ` I ) ` ( s u. t ) ) = ( ( D ` I ) ` ( s u. t ) )
104 1 2 92 93 94 102 103 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 ) ) ) ) )
105 simpl1 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ph )
106 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
107 106 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
108 105 107 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 ) ) )
109 104 108 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 ) ) )
110 simprl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
111 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
112 1 2 92 93 94 110 111 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 ) ) ) )
113 106 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` s ) = ( K ` s ) )
114 105 113 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 ) )
115 112 114 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 ) )
116 simprr 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
117 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
118 1 2 92 93 94 116 117 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 ) ) ) )
119 106 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` t ) = ( K ` t ) )
120 105 119 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 ) )
121 118 120 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 ) )
122 115 121 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 ) ) )
123 109 122 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 ) ) ) )
124 65 88 89 90 91 123 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 ) ) ) )
125 84 87 124 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 ) ) ) )
126 56 64 125 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 ) ) ) )
127 35 49 126 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 ) ) ) )
128 18 31 127 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 ) ) ) )
129 14 128 bitrid 
 |-  ( 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 ) ) ) )