Metamath Proof Explorer

Theorem ntrclsk13

Description: The interior of the intersection of any pair is equal to the intersection of the interiors if and only if the closure of the unions of any pair is equal to the union of closures. (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 ntrclsk13 
|- ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) = ( ( 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 ineq1 
 |-  ( s = a -> ( s i^i t ) = ( a i^i t ) )
5 4 fveq2d 
 |-  ( s = a -> ( I ` ( s i^i t ) ) = ( I ` ( a i^i t ) ) )
6 fveq2 
 |-  ( s = a -> ( I ` s ) = ( I ` a ) )
7 6 ineq1d 
 |-  ( s = a -> ( ( I ` s ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` t ) ) )
8 5 7 eqeq12d 
 |-  ( s = a -> ( ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> ( I ` ( a i^i t ) ) = ( ( I ` a ) i^i ( I ` t ) ) ) )
9 ineq2 
 |-  ( t = b -> ( a i^i t ) = ( a i^i b ) )
10 9 fveq2d 
 |-  ( t = b -> ( I ` ( a i^i t ) ) = ( I ` ( a i^i b ) ) )
11 fveq2 
 |-  ( t = b -> ( I ` t ) = ( I ` b ) )
12 11 ineq2d 
 |-  ( t = b -> ( ( I ` a ) i^i ( I ` t ) ) = ( ( I ` a ) i^i ( I ` b ) ) )
13 10 12 eqeq12d 
 |-  ( t = b -> ( ( I ` ( a i^i t ) ) = ( ( I ` a ) i^i ( I ` t ) ) <-> ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) ) )
14 8 13 cbvral2vw 
 |-  ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. a e. ~P B A. b e. ~P B ( I ` ( a i^i b ) ) = ( ( I ` a ) i^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 15 adantr 
 |-  ( ( ph /\ a C_ B ) -> B e. _V )
21 difssd 
 |-  ( ( ph /\ a C_ B ) -> ( B \ a ) C_ B )
22 20 21 sselpwd 
 |-  ( ( ph /\ a C_ B ) -> ( B \ a ) e. ~P B )
23 difeq2 
 |-  ( s = ( B \ a ) -> ( B \ s ) = ( B \ ( B \ a ) ) )
24 23 eqeq2d 
 |-  ( s = ( B \ a ) -> ( a = ( B \ s ) <-> a = ( B \ ( B \ a ) ) ) )
25 eqcom 
 |-  ( a = ( B \ ( B \ a ) ) <-> ( B \ ( B \ a ) ) = a )
26 24 25 bitrdi 
 |-  ( s = ( B \ a ) -> ( a = ( B \ s ) <-> ( B \ ( B \ a ) ) = a ) )
27 26 adantl 
 |-  ( ( ( ph /\ 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 
 |-  ( ( ph /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
30 22 27 29 rspcedvd 
 |-  ( ( ph /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
31 19 30 sylan2 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
32 ineq1 
 |-  ( a = ( B \ s ) -> ( a i^i b ) = ( ( B \ s ) i^i b ) )
33 32 fveq2d 
 |-  ( a = ( B \ s ) -> ( I ` ( a i^i b ) ) = ( I ` ( ( B \ s ) i^i b ) ) )
34 fveq2 
 |-  ( a = ( B \ s ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
35 34 ineq1d 
 |-  ( a = ( B \ s ) -> ( ( I ` a ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) )
36 33 35 eqeq12d 
 |-  ( a = ( B \ s ) -> ( ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) <-> ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) ) )
37 36 ralbidv 
 |-  ( a = ( B \ s ) -> ( A. b e. ~P B ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) <-> A. b e. ~P B ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) ) )
38 37 3ad2ant3 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) <-> A. b e. ~P B ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) ) )
39 difssd 
 |-  ( ph -> ( B \ t ) C_ B )
40 15 39 sselpwd 
 |-  ( ph -> ( B \ t ) e. ~P B )
41 40 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
42 simpll 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> ph )
43 elpwi 
 |-  ( b e. ~P B -> b C_ B )
44 43 adantl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> b C_ B )
45 difssd 
 |-  ( ph -> ( B \ b ) C_ B )
46 15 45 sselpwd 
 |-  ( ph -> ( B \ b ) e. ~P B )
47 46 adantr 
 |-  ( ( ph /\ b C_ B ) -> ( B \ b ) e. ~P B )
48 difeq2 
 |-  ( t = ( B \ b ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
49 48 eqeq2d 
 |-  ( t = ( B \ b ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
50 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
51 49 50 bitrdi 
 |-  ( t = ( B \ b ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
52 51 adantl 
 |-  ( ( ( ph /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
53 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
54 53 bilani 
 |-  ( ( ph /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
55 47 52 54 rspcedvd 
 |-  ( ( ph /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
56 42 44 55 syl2anc 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> E. t e. ~P B b = ( B \ t ) )
57 ineq2 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( ( B \ s ) i^i ( B \ t ) ) )
58 difundi 
 |-  ( B \ ( s u. t ) ) = ( ( B \ s ) i^i ( B \ t ) )
59 57 58 eqtr4di 
 |-  ( b = ( B \ t ) -> ( ( B \ s ) i^i b ) = ( B \ ( s u. t ) ) )
60 59 fveq2d 
 |-  ( b = ( B \ t ) -> ( I ` ( ( B \ s ) i^i b ) ) = ( I ` ( B \ ( s u. t ) ) ) )
61 fveq2 
 |-  ( b = ( B \ t ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
62 61 ineq2d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) )
63 60 62 eqeq12d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) <-> ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) )
64 63 3ad2ant3 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) <-> ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) )
65 simp1l 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
66 65 15 jccir 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ph /\ B e. _V ) )
67 simp1r 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
68 simp2 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
69 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
70 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
71 69 70 syl 
 |-  ( ph -> I : ~P B --> ~P B )
72 71 anim1i 
 |-  ( ( ph /\ B e. _V ) -> ( I : ~P B --> ~P B /\ B e. _V ) )
73 72 adantr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( I : ~P B --> ~P B /\ B e. _V ) )
74 simpl 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> I : ~P B --> ~P B )
75 simpr 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> B e. _V )
76 difssd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ ( s u. t ) ) C_ B )
77 75 76 sselpwd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ ( s u. t ) ) e. ~P B )
78 74 77 ffvelcdmd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) e. ~P B )
79 78 elpwid 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) C_ B )
80 difssd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ s ) C_ B )
81 75 80 sselpwd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ s ) e. ~P B )
82 74 81 ffvelcdmd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ s ) ) e. ~P B )
83 82 elpwid 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ s ) ) C_ B )
84 ssinss1 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
85 83 84 syl 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
86 79 85 jca 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( ( I ` ( B \ ( s u. t ) ) ) C_ B /\ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B ) )
87 rcompleq 
 |-  ( ( ( I ` ( B \ ( s u. t ) ) ) C_ B /\ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B ) -> ( ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) = ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) ) )
88 73 86 87 3syl 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) = ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) ) )
89 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
90 69 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> I e. ( ~P B ^m ~P B ) )
91 eqid 
 |-  ( D ` I ) = ( D ` I )
92 simprl 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
93 92 elpwid 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s C_ B )
94 simprr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
95 94 elpwid 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t C_ B )
96 93 95 unssd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) C_ B )
97 89 96 sselpwd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
98 eqid 
 |-  ( ( D ` I ) ` ( s u. t ) ) = ( ( D ` I ) ` ( s u. t ) )
99 1 2 89 90 91 97 98 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` ( s u. t ) ) = ( B \ ( I ` ( B \ ( s u. t ) ) ) ) )
100 simpl 
 |-  ( ( s e. ~P B /\ t e. ~P B ) -> s e. ~P B )
101 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> B e. _V )
102 69 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
103 simpr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> s e. ~P B )
104 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
105 1 2 101 102 91 103 104 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
106 100 105 sylan2 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
107 simpr 
 |-  ( ( s e. ~P B /\ t e. ~P B ) -> t e. ~P B )
108 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> B e. _V )
109 69 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
110 simpr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> t e. ~P B )
111 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
112 1 2 108 109 91 110 111 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
113 107 112 sylan2 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
114 106 113 uneq12d 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) ) )
115 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
116 114 115 eqtr4di 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) )
117 99 116 eqeq12d 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( ( D ` I ) ` ( s u. t ) ) = ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) <-> ( B \ ( I ` ( B \ ( s u. t ) ) ) ) = ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) ) )
118 simpll 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ph )
119 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
120 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
121 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` s ) = ( K ` s ) )
122 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` t ) = ( K ` t ) )
123 121 122 uneq12d 
 |-  ( ( D ` I ) = K -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( K ` s ) u. ( K ` t ) ) )
124 120 123 eqeq12d 
 |-  ( ( D ` I ) = K -> ( ( ( D ` I ) ` ( s u. t ) ) = ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) <-> ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
125 118 119 124 3syl 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( ( D ` I ) ` ( s u. t ) ) = ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) <-> ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
126 88 117 125 3bitr2d 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) <-> ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
127 66 67 68 126 syl12anc 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( I ` ( B \ ( s u. t ) ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) <-> ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
128 64 127 bitrd 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) <-> ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
129 41 56 128 ralxfrd2 
 |-  ( ( ph /\ s e. ~P B ) -> ( A. b e. ~P B ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) <-> A. t e. ~P B ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
130 129 3adant3 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( I ` ( ( B \ s ) i^i b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) <-> A. t e. ~P B ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
131 38 130 bitrd 
 |-  ( ( ph /\ s e. ~P B /\ a = ( B \ s ) ) -> ( A. b e. ~P B ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) <-> A. t e. ~P B ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
132 18 31 131 ralxfrd2 
 |-  ( ph -> ( A. a e. ~P B A. b e. ~P B ( I ` ( a i^i b ) ) = ( ( I ` a ) i^i ( I ` b ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )
133 14 132 bitrid 
 |-  ( ph -> ( A. s e. ~P B A. t e. ~P B ( I ` ( s i^i t ) ) = ( ( I ` s ) i^i ( I ` t ) ) <-> A. s e. ~P B A. t e. ~P B ( K ` ( s u. t ) ) = ( ( K ` s ) u. ( K ` t ) ) ) )