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 biimpi 
 |-  ( a C_ B -> ( B \ ( B \ a ) ) = a )
30 29 adantl 
 |-  ( ( ph /\ a C_ B ) -> ( B \ ( B \ a ) ) = a )
31 22 27 30 rspcedvd 
 |-  ( ( ph /\ a C_ B ) -> E. s e. ~P B a = ( B \ s ) )
32 19 31 sylan2 
 |-  ( ( ph /\ a e. ~P B ) -> E. s e. ~P B a = ( B \ s ) )
33 ineq1 
 |-  ( a = ( B \ s ) -> ( a i^i b ) = ( ( B \ s ) i^i b ) )
34 33 fveq2d 
 |-  ( a = ( B \ s ) -> ( I ` ( a i^i b ) ) = ( I ` ( ( B \ s ) i^i b ) ) )
35 fveq2 
 |-  ( a = ( B \ s ) -> ( I ` a ) = ( I ` ( B \ s ) ) )
36 35 ineq1d 
 |-  ( a = ( B \ s ) -> ( ( I ` a ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) )
37 34 36 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 ) ) ) )
38 37 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 ) ) ) )
39 38 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 ) ) ) )
40 difssd 
 |-  ( ph -> ( B \ t ) C_ B )
41 15 40 sselpwd 
 |-  ( ph -> ( B \ t ) e. ~P B )
42 41 ad2antrr 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B ) -> ( B \ t ) e. ~P B )
43 simpll 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> ph )
44 elpwi 
 |-  ( b e. ~P B -> b C_ B )
45 44 adantl 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> b C_ B )
46 difssd 
 |-  ( ph -> ( B \ b ) C_ B )
47 15 46 sselpwd 
 |-  ( ph -> ( B \ b ) e. ~P B )
48 47 adantr 
 |-  ( ( ph /\ b C_ B ) -> ( B \ b ) e. ~P B )
49 difeq2 
 |-  ( t = ( B \ b ) -> ( B \ t ) = ( B \ ( B \ b ) ) )
50 49 eqeq2d 
 |-  ( t = ( B \ b ) -> ( b = ( B \ t ) <-> b = ( B \ ( B \ b ) ) ) )
51 eqcom 
 |-  ( b = ( B \ ( B \ b ) ) <-> ( B \ ( B \ b ) ) = b )
52 50 51 bitrdi 
 |-  ( t = ( B \ b ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
53 52 adantl 
 |-  ( ( ( ph /\ b C_ B ) /\ t = ( B \ b ) ) -> ( b = ( B \ t ) <-> ( B \ ( B \ b ) ) = b ) )
54 dfss4 
 |-  ( b C_ B <-> ( B \ ( B \ b ) ) = b )
55 54 biimpi 
 |-  ( b C_ B -> ( B \ ( B \ b ) ) = b )
56 55 adantl 
 |-  ( ( ph /\ b C_ B ) -> ( B \ ( B \ b ) ) = b )
57 48 53 56 rspcedvd 
 |-  ( ( ph /\ b C_ B ) -> E. t e. ~P B b = ( B \ t ) )
58 43 45 57 syl2anc 
 |-  ( ( ( ph /\ s e. ~P B ) /\ b e. ~P B ) -> E. t e. ~P B b = ( 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 fveq2 
 |-  ( b = ( B \ t ) -> ( I ` b ) = ( I ` ( B \ t ) ) )
64 63 ineq2d 
 |-  ( b = ( B \ t ) -> ( ( I ` ( B \ s ) ) i^i ( I ` b ) ) = ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) )
65 62 64 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 ) ) ) ) )
66 65 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 ) ) ) ) )
67 simp1l 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ph )
68 67 15 jccir 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> ( ph /\ B e. _V ) )
69 simp1r 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> s e. ~P B )
70 simp2 
 |-  ( ( ( ph /\ s e. ~P B ) /\ t e. ~P B /\ b = ( B \ t ) ) -> t e. ~P B )
71 1 2 3 ntrclsiex 
 |-  ( ph -> I e. ( ~P B ^m ~P B ) )
72 elmapi 
 |-  ( I e. ( ~P B ^m ~P B ) -> I : ~P B --> ~P B )
73 71 72 syl 
 |-  ( ph -> I : ~P B --> ~P B )
74 73 anim1i 
 |-  ( ( ph /\ B e. _V ) -> ( I : ~P B --> ~P B /\ B e. _V ) )
75 74 adantr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( I : ~P B --> ~P B /\ B e. _V ) )
76 simpl 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> I : ~P B --> ~P B )
77 simpr 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> B e. _V )
78 difssd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ ( s u. t ) ) C_ B )
79 77 78 sselpwd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ ( s u. t ) ) e. ~P B )
80 76 79 ffvelcdmd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) e. ~P B )
81 80 elpwid 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ ( s u. t ) ) ) C_ B )
82 difssd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ s ) C_ B )
83 77 82 sselpwd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( B \ s ) e. ~P B )
84 76 83 ffvelcdmd 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ s ) ) e. ~P B )
85 84 elpwid 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( I ` ( B \ s ) ) C_ B )
86 ssinss1 
 |-  ( ( I ` ( B \ s ) ) C_ B -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
87 85 86 syl 
 |-  ( ( I : ~P B --> ~P B /\ B e. _V ) -> ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) C_ B )
88 81 87 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 ) )
89 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 ) ) ) ) ) )
90 75 88 89 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 ) ) ) ) ) )
91 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> B e. _V )
92 71 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> I e. ( ~P B ^m ~P B ) )
93 eqid 
 |-  ( D ` I ) = ( D ` I )
94 simprl 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s e. ~P B )
95 94 elpwid 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> s C_ B )
96 simprr 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t e. ~P B )
97 96 elpwid 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> t C_ B )
98 95 97 unssd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) C_ B )
99 91 98 sselpwd 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( s u. t ) e. ~P B )
100 eqid 
 |-  ( ( D ` I ) ` ( s u. t ) ) = ( ( D ` I ) ` ( s u. t ) )
101 1 2 91 92 93 99 100 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` ( s u. t ) ) = ( B \ ( I ` ( B \ ( s u. t ) ) ) ) )
102 simpl 
 |-  ( ( s e. ~P B /\ t e. ~P B ) -> s e. ~P B )
103 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> B e. _V )
104 71 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
105 simpr 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> s e. ~P B )
106 eqid 
 |-  ( ( D ` I ) ` s ) = ( ( D ` I ) ` s )
107 1 2 103 104 93 105 106 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ s e. ~P B ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
108 102 107 sylan2 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` s ) = ( B \ ( I ` ( B \ s ) ) ) )
109 simpr 
 |-  ( ( s e. ~P B /\ t e. ~P B ) -> t e. ~P B )
110 simplr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> B e. _V )
111 71 ad2antrr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> I e. ( ~P B ^m ~P B ) )
112 simpr 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> t e. ~P B )
113 eqid 
 |-  ( ( D ` I ) ` t ) = ( ( D ` I ) ` t )
114 1 2 110 111 93 112 113 dssmapfv3d 
 |-  ( ( ( ph /\ B e. _V ) /\ t e. ~P B ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
115 109 114 sylan2 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ( ( D ` I ) ` t ) = ( B \ ( I ` ( B \ t ) ) ) )
116 108 115 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 ) ) ) ) )
117 difindi 
 |-  ( B \ ( ( I ` ( B \ s ) ) i^i ( I ` ( B \ t ) ) ) ) = ( ( B \ ( I ` ( B \ s ) ) ) u. ( B \ ( I ` ( B \ t ) ) ) )
118 116 117 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 ) ) ) ) )
119 101 118 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 ) ) ) ) ) )
120 simpll 
 |-  ( ( ( ph /\ B e. _V ) /\ ( s e. ~P B /\ t e. ~P B ) ) -> ph )
121 1 2 3 ntrclsfv1 
 |-  ( ph -> ( D ` I ) = K )
122 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` ( s u. t ) ) = ( K ` ( s u. t ) ) )
123 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` s ) = ( K ` s ) )
124 fveq1 
 |-  ( ( D ` I ) = K -> ( ( D ` I ) ` t ) = ( K ` t ) )
125 123 124 uneq12d 
 |-  ( ( D ` I ) = K -> ( ( ( D ` I ) ` s ) u. ( ( D ` I ) ` t ) ) = ( ( K ` s ) u. ( K ` t ) ) )
126 122 125 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 ) ) ) )
127 120 121 126 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 ) ) ) )
128 90 119 127 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 ) ) ) )
129 68 69 70 128 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 ) ) ) )
130 66 129 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 ) ) ) )
131 42 58 130 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 ) ) ) )
132 131 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 ) ) ) )
133 39 132 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 ) ) ) )
134 18 32 133 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 ) ) ) )
135 14 134 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 ) ) ) )