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 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
71 70 adantr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> I : ~P B --> ~P B )
72 simpr 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> B e. _V )
73 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) C_ B )
74 72 73 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ s ) e. ~P B )
75 71 74 ffvelcdmd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) e. ~P B )
76 75 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ s ) ) C_ B )
77 orc 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) )
78 inss 
 |-  ( ( ( I ` ( B \ s ) ) C_ B \/ ( I ` ( B \ t ) ) C_ B ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
79 76 77 78 3syl 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
80 difssd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) C_ B )
81 72 80 sselpwd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( B \ ( s u. t ) ) e. ~P B )
82 71 81 ffvelcdmd 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) e. ~P B )
83 82 elpwid 
 |-  ( ( I e. ( ~P B ^m ~P B ) /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) C_ B )
84 79 83 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 ) )
85 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 ) ) ) ) ) )
86 67 69 84 85 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 ) ) ) ) ) )
87 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
88 87 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 ) ) ) ) )
89 88 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 ) ) ) ) ) )
90 67 15 syl 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> B e. _V )
91 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 ) )
92 simp12 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
93 rp-simp2 
 |-  ( ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
94 simpl2 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
95 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 ) )
96 eqid 
 |-  ( D ` I ) = ( D ` I )
97 simpl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
98 simprl 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
99 98 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> s C_ B )
100 simprr 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
101 100 elpwid 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> t C_ B )
102 99 101 unssd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) C_ B )
103 97 102 sselpwd 
 |-  ( ( B e. _V /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
104 103 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 )
105 eqid 
 |-  ( ( D ` I ) ` ( s u. t ) ) = ( ( D ` I ) ` ( s u. t ) )
106 1 2 94 95 96 104 105 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 ) ) ) ) )
107 simpl1 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ph )
108 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
109 108 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
110 107 109 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 ) ) )
111 106 110 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 ) ) )
112 simprl 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
113 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
114 1 2 94 95 96 112 113 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 ) ) ) )
115 108 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` s ) = ( K ` s ) )
116 107 115 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 ) )
117 114 116 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 ) )
118 simprr 
 |-  ( ( ( ph /\ B e. _V /\ I e. ( ~P B ^m ~P B ) ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
119 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
120 1 2 94 95 96 118 119 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 ) ) ) )
121 108 fveq1d 
 |-  ( ph -> ( ( D ` I ) ` t ) = ( K ` t ) )
122 107 121 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 ) )
123 120 122 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 ) )
124 117 123 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 ) ) )
125 111 124 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 ) ) ) )
126 67 90 91 92 93 125 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 ) ) ) )
127 86 89 126 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 ) ) ) )
128 58 66 127 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 ) ) ) )
129 36 51 128 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 ) ) ) )
130 18 32 129 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 ) ) ) )
131 14 130 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 ) ) ) )