Metamath Proof Explorer

Theorem cvmliftmolem1

Description: Lemma for cvmliftmo . (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses cvmliftmo.b 
|- B = U. C
cvmliftmo.y 
|- Y = U. K
cvmliftmo.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftmo.k 
|- ( ph -> K e. Conn )
cvmliftmo.l 
|- ( ph -> K e. N-Locally Conn )
cvmliftmo.o 
|- ( ph -> O e. Y )
cvmliftmoi.m 
|- ( ph -> M e. ( K Cn C ) )
cvmliftmoi.n 
|- ( ph -> N e. ( K Cn C ) )
cvmliftmoi.g 
|- ( ph -> ( F o. M ) = ( F o. N ) )
cvmliftmoi.p 
|- ( ph -> ( M ` O ) = ( N ` O ) )
cvmliftmolem.1 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
cvmliftmolem.2 
|- ( ( ph /\ ps ) -> T e. ( S ` U ) )
cvmliftmolem.3 
|- ( ( ph /\ ps ) -> W e. T )
cvmliftmolem.4 
|- ( ( ph /\ ps ) -> I C_ ( `' M " W ) )
cvmliftmolem.5 
|- ( ( ph /\ ps ) -> ( K |`t I ) e. Conn )
cvmliftmolem.6 
|- ( ( ph /\ ps ) -> X e. I )
cvmliftmolem.7 
|- ( ( ph /\ ps ) -> Q e. I )
cvmliftmolem.8 
|- ( ( ph /\ ps ) -> R e. I )
cvmliftmolem.9 
|- ( ( ph /\ ps ) -> ( F ` ( M ` X ) ) e. U )
Assertion cvmliftmolem1 
|- ( ( ph /\ ps ) -> ( Q e. dom ( M i^i N ) -> R e. dom ( M i^i N ) ) )

Proof

Step Hyp Ref Expression
1 cvmliftmo.b 
 |-  B = U. C
2 cvmliftmo.y 
 |-  Y = U. K
3 cvmliftmo.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmliftmo.k 
 |-  ( ph -> K e. Conn )
5 cvmliftmo.l 
 |-  ( ph -> K e. N-Locally Conn )
6 cvmliftmo.o 
 |-  ( ph -> O e. Y )
7 cvmliftmoi.m 
 |-  ( ph -> M e. ( K Cn C ) )
8 cvmliftmoi.n 
 |-  ( ph -> N e. ( K Cn C ) )
9 cvmliftmoi.g 
 |-  ( ph -> ( F o. M ) = ( F o. N ) )
10 cvmliftmoi.p 
 |-  ( ph -> ( M ` O ) = ( N ` O ) )
11 cvmliftmolem.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
12 cvmliftmolem.2 
 |-  ( ( ph /\ ps ) -> T e. ( S ` U ) )
13 cvmliftmolem.3 
 |-  ( ( ph /\ ps ) -> W e. T )
14 cvmliftmolem.4 
 |-  ( ( ph /\ ps ) -> I C_ ( `' M " W ) )
15 cvmliftmolem.5 
 |-  ( ( ph /\ ps ) -> ( K |`t I ) e. Conn )
16 cvmliftmolem.6 
 |-  ( ( ph /\ ps ) -> X e. I )
17 cvmliftmolem.7 
 |-  ( ( ph /\ ps ) -> Q e. I )
18 cvmliftmolem.8 
 |-  ( ( ph /\ ps ) -> R e. I )
19 cvmliftmolem.9 
 |-  ( ( ph /\ ps ) -> ( F ` ( M ` X ) ) e. U )
20 9 adantr 
 |-  ( ( ph /\ ps ) -> ( F o. M ) = ( F o. N ) )
21 20 fveq1d 
 |-  ( ( ph /\ ps ) -> ( ( F o. M ) ` R ) = ( ( F o. N ) ` R ) )
22 14 18 sseldd 
 |-  ( ( ph /\ ps ) -> R e. ( `' M " W ) )
23 2 1 cnf 
 |-  ( M e. ( K Cn C ) -> M : Y --> B )
24 7 23 syl 
 |-  ( ph -> M : Y --> B )
25 24 ffnd 
 |-  ( ph -> M Fn Y )
26 elpreima 
 |-  ( M Fn Y -> ( R e. ( `' M " W ) <-> ( R e. Y /\ ( M ` R ) e. W ) ) )
27 25 26 syl 
 |-  ( ph -> ( R e. ( `' M " W ) <-> ( R e. Y /\ ( M ` R ) e. W ) ) )
28 27 simprbda 
 |-  ( ( ph /\ R e. ( `' M " W ) ) -> R e. Y )
29 22 28 syldan 
 |-  ( ( ph /\ ps ) -> R e. Y )
30 fvco3 
 |-  ( ( M : Y --> B /\ R e. Y ) -> ( ( F o. M ) ` R ) = ( F ` ( M ` R ) ) )
31 24 30 sylan 
 |-  ( ( ph /\ R e. Y ) -> ( ( F o. M ) ` R ) = ( F ` ( M ` R ) ) )
32 29 31 syldan 
 |-  ( ( ph /\ ps ) -> ( ( F o. M ) ` R ) = ( F ` ( M ` R ) ) )
33 2 1 cnf 
 |-  ( N e. ( K Cn C ) -> N : Y --> B )
34 8 33 syl 
 |-  ( ph -> N : Y --> B )
35 fvco3 
 |-  ( ( N : Y --> B /\ R e. Y ) -> ( ( F o. N ) ` R ) = ( F ` ( N ` R ) ) )
36 34 35 sylan 
 |-  ( ( ph /\ R e. Y ) -> ( ( F o. N ) ` R ) = ( F ` ( N ` R ) ) )
37 29 36 syldan 
 |-  ( ( ph /\ ps ) -> ( ( F o. N ) ` R ) = ( F ` ( N ` R ) ) )
38 21 32 37 3eqtr3d 
 |-  ( ( ph /\ ps ) -> ( F ` ( M ` R ) ) = ( F ` ( N ` R ) ) )
39 38 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( F ` ( M ` R ) ) = ( F ` ( N ` R ) ) )
40 27 simplbda 
 |-  ( ( ph /\ R e. ( `' M " W ) ) -> ( M ` R ) e. W )
41 22 40 syldan 
 |-  ( ( ph /\ ps ) -> ( M ` R ) e. W )
42 41 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( M ` R ) e. W )
43 fvres 
 |-  ( ( M ` R ) e. W -> ( ( F |` W ) ` ( M ` R ) ) = ( F ` ( M ` R ) ) )
44 42 43 syl 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( F |` W ) ` ( M ` R ) ) = ( F ` ( M ` R ) ) )
45 18 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> R e. I )
46 fvres 
 |-  ( R e. I -> ( ( N |` I ) ` R ) = ( N ` R ) )
47 45 46 syl 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( N |` I ) ` R ) = ( N ` R ) )
48 eqid 
 |-  U. ( K |`t I ) = U. ( K |`t I )
49 15 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( K |`t I ) e. Conn )
50 8 adantr 
 |-  ( ( ph /\ ps ) -> N e. ( K Cn C ) )
51 cnvimass 
 |-  ( `' M " W ) C_ dom M
52 51 24 fssdm 
 |-  ( ph -> ( `' M " W ) C_ Y )
53 52 adantr 
 |-  ( ( ph /\ ps ) -> ( `' M " W ) C_ Y )
54 14 53 sstrd 
 |-  ( ( ph /\ ps ) -> I C_ Y )
55 2 cnrest 
 |-  ( ( N e. ( K Cn C ) /\ I C_ Y ) -> ( N |` I ) e. ( ( K |`t I ) Cn C ) )
56 50 54 55 syl2anc 
 |-  ( ( ph /\ ps ) -> ( N |` I ) e. ( ( K |`t I ) Cn C ) )
57 3 adantr 
 |-  ( ( ph /\ ps ) -> F e. ( C CovMap J ) )
58 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
59 57 58 syl 
 |-  ( ( ph /\ ps ) -> C e. Top )
60 1 toptopon 
 |-  ( C e. Top <-> C e. ( TopOn ` B ) )
61 59 60 sylib 
 |-  ( ( ph /\ ps ) -> C e. ( TopOn ` B ) )
62 df-ima 
 |-  ( N " I ) = ran ( N |` I )
63 elssuni 
 |-  ( W e. T -> W C_ U. T )
64 13 63 syl 
 |-  ( ( ph /\ ps ) -> W C_ U. T )
65 11 cvmsuni 
 |-  ( T e. ( S ` U ) -> U. T = ( `' F " U ) )
66 12 65 syl 
 |-  ( ( ph /\ ps ) -> U. T = ( `' F " U ) )
67 64 66 sseqtrd 
 |-  ( ( ph /\ ps ) -> W C_ ( `' F " U ) )
68 imass2 
 |-  ( W C_ ( `' F " U ) -> ( `' M " W ) C_ ( `' M " ( `' F " U ) ) )
69 67 68 syl 
 |-  ( ( ph /\ ps ) -> ( `' M " W ) C_ ( `' M " ( `' F " U ) ) )
70 14 69 sstrd 
 |-  ( ( ph /\ ps ) -> I C_ ( `' M " ( `' F " U ) ) )
71 20 cnveqd 
 |-  ( ( ph /\ ps ) -> `' ( F o. M ) = `' ( F o. N ) )
72 cnvco 
 |-  `' ( F o. M ) = ( `' M o. `' F )
73 cnvco 
 |-  `' ( F o. N ) = ( `' N o. `' F )
74 71 72 73 3eqtr3g 
 |-  ( ( ph /\ ps ) -> ( `' M o. `' F ) = ( `' N o. `' F ) )
75 74 imaeq1d 
 |-  ( ( ph /\ ps ) -> ( ( `' M o. `' F ) " U ) = ( ( `' N o. `' F ) " U ) )
76 imaco 
 |-  ( ( `' M o. `' F ) " U ) = ( `' M " ( `' F " U ) )
77 imaco 
 |-  ( ( `' N o. `' F ) " U ) = ( `' N " ( `' F " U ) )
78 75 76 77 3eqtr3g 
 |-  ( ( ph /\ ps ) -> ( `' M " ( `' F " U ) ) = ( `' N " ( `' F " U ) ) )
79 70 78 sseqtrd 
 |-  ( ( ph /\ ps ) -> I C_ ( `' N " ( `' F " U ) ) )
80 34 adantr 
 |-  ( ( ph /\ ps ) -> N : Y --> B )
81 80 ffund 
 |-  ( ( ph /\ ps ) -> Fun N )
82 80 fdmd 
 |-  ( ( ph /\ ps ) -> dom N = Y )
83 54 82 sseqtrrd 
 |-  ( ( ph /\ ps ) -> I C_ dom N )
84 funimass3 
 |-  ( ( Fun N /\ I C_ dom N ) -> ( ( N " I ) C_ ( `' F " U ) <-> I C_ ( `' N " ( `' F " U ) ) ) )
85 81 83 84 syl2anc 
 |-  ( ( ph /\ ps ) -> ( ( N " I ) C_ ( `' F " U ) <-> I C_ ( `' N " ( `' F " U ) ) ) )
86 79 85 mpbird 
 |-  ( ( ph /\ ps ) -> ( N " I ) C_ ( `' F " U ) )
87 62 86 eqsstrrid 
 |-  ( ( ph /\ ps ) -> ran ( N |` I ) C_ ( `' F " U ) )
88 cnvimass 
 |-  ( `' F " U ) C_ dom F
89 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
90 3 89 syl 
 |-  ( ph -> F e. ( C Cn J ) )
91 eqid 
 |-  U. J = U. J
92 1 91 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
93 90 92 syl 
 |-  ( ph -> F : B --> U. J )
94 93 fdmd 
 |-  ( ph -> dom F = B )
95 94 adantr 
 |-  ( ( ph /\ ps ) -> dom F = B )
96 88 95 sseqtrid 
 |-  ( ( ph /\ ps ) -> ( `' F " U ) C_ B )
97 cnrest2 
 |-  ( ( C e. ( TopOn ` B ) /\ ran ( N |` I ) C_ ( `' F " U ) /\ ( `' F " U ) C_ B ) -> ( ( N |` I ) e. ( ( K |`t I ) Cn C ) <-> ( N |` I ) e. ( ( K |`t I ) Cn ( C |`t ( `' F " U ) ) ) ) )
98 61 87 96 97 syl3anc 
 |-  ( ( ph /\ ps ) -> ( ( N |` I ) e. ( ( K |`t I ) Cn C ) <-> ( N |` I ) e. ( ( K |`t I ) Cn ( C |`t ( `' F " U ) ) ) ) )
99 56 98 mpbid 
 |-  ( ( ph /\ ps ) -> ( N |` I ) e. ( ( K |`t I ) Cn ( C |`t ( `' F " U ) ) ) )
100 99 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( N |` I ) e. ( ( K |`t I ) Cn ( C |`t ( `' F " U ) ) ) )
101 df-ss 
 |-  ( W C_ ( `' F " U ) <-> ( W i^i ( `' F " U ) ) = W )
102 67 101 sylib 
 |-  ( ( ph /\ ps ) -> ( W i^i ( `' F " U ) ) = W )
103 1 topopn 
 |-  ( C e. Top -> B e. C )
104 59 103 syl 
 |-  ( ( ph /\ ps ) -> B e. C )
105 104 96 ssexd 
 |-  ( ( ph /\ ps ) -> ( `' F " U ) e. _V )
106 11 cvmsss 
 |-  ( T e. ( S ` U ) -> T C_ C )
107 12 106 syl 
 |-  ( ( ph /\ ps ) -> T C_ C )
108 107 13 sseldd 
 |-  ( ( ph /\ ps ) -> W e. C )
109 elrestr 
 |-  ( ( C e. Top /\ ( `' F " U ) e. _V /\ W e. C ) -> ( W i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) )
110 59 105 108 109 syl3anc 
 |-  ( ( ph /\ ps ) -> ( W i^i ( `' F " U ) ) e. ( C |`t ( `' F " U ) ) )
111 102 110 eqeltrrd 
 |-  ( ( ph /\ ps ) -> W e. ( C |`t ( `' F " U ) ) )
112 111 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> W e. ( C |`t ( `' F " U ) ) )
113 11 cvmscld 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ W e. T ) -> W e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )
114 57 12 13 113 syl3anc 
 |-  ( ( ph /\ ps ) -> W e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )
115 114 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> W e. ( Clsd ` ( C |`t ( `' F " U ) ) ) )
116 conntop 
 |-  ( K e. Conn -> K e. Top )
117 4 116 syl 
 |-  ( ph -> K e. Top )
118 117 adantr 
 |-  ( ( ph /\ ps ) -> K e. Top )
119 2 restuni 
 |-  ( ( K e. Top /\ I C_ Y ) -> I = U. ( K |`t I ) )
120 118 54 119 syl2anc 
 |-  ( ( ph /\ ps ) -> I = U. ( K |`t I ) )
121 17 120 eleqtrd 
 |-  ( ( ph /\ ps ) -> Q e. U. ( K |`t I ) )
122 121 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> Q e. U. ( K |`t I ) )
123 17 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> Q e. I )
124 fvres 
 |-  ( Q e. I -> ( ( N |` I ) ` Q ) = ( N ` Q ) )
125 123 124 syl 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( N |` I ) ` Q ) = ( N ` Q ) )
126 simpr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( M ` Q ) = ( N ` Q ) )
127 14 17 sseldd 
 |-  ( ( ph /\ ps ) -> Q e. ( `' M " W ) )
128 elpreima 
 |-  ( M Fn Y -> ( Q e. ( `' M " W ) <-> ( Q e. Y /\ ( M ` Q ) e. W ) ) )
129 25 128 syl 
 |-  ( ph -> ( Q e. ( `' M " W ) <-> ( Q e. Y /\ ( M ` Q ) e. W ) ) )
130 129 simplbda 
 |-  ( ( ph /\ Q e. ( `' M " W ) ) -> ( M ` Q ) e. W )
131 127 130 syldan 
 |-  ( ( ph /\ ps ) -> ( M ` Q ) e. W )
132 131 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( M ` Q ) e. W )
133 126 132 eqeltrrd 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( N ` Q ) e. W )
134 125 133 eqeltrd 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( N |` I ) ` Q ) e. W )
135 48 49 100 112 115 122 134 conncn 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( N |` I ) : U. ( K |`t I ) --> W )
136 120 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> I = U. ( K |`t I ) )
137 136 feq2d 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( N |` I ) : I --> W <-> ( N |` I ) : U. ( K |`t I ) --> W ) )
138 135 137 mpbird 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( N |` I ) : I --> W )
139 138 45 ffvelrnd 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( N |` I ) ` R ) e. W )
140 47 139 eqeltrrd 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( N ` R ) e. W )
141 fvres 
 |-  ( ( N ` R ) e. W -> ( ( F |` W ) ` ( N ` R ) ) = ( F ` ( N ` R ) ) )
142 140 141 syl 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( F |` W ) ` ( N ` R ) ) = ( F ` ( N ` R ) ) )
143 39 44 142 3eqtr4d 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( F |` W ) ` ( M ` R ) ) = ( ( F |` W ) ` ( N ` R ) ) )
144 11 cvmsf1o 
 |-  ( ( F e. ( C CovMap J ) /\ T e. ( S ` U ) /\ W e. T ) -> ( F |` W ) : W -1-1-onto-> U )
145 57 12 13 144 syl3anc 
 |-  ( ( ph /\ ps ) -> ( F |` W ) : W -1-1-onto-> U )
146 f1of1 
 |-  ( ( F |` W ) : W -1-1-onto-> U -> ( F |` W ) : W -1-1-> U )
147 145 146 syl 
 |-  ( ( ph /\ ps ) -> ( F |` W ) : W -1-1-> U )
148 147 adantr 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( F |` W ) : W -1-1-> U )
149 f1fveq 
 |-  ( ( ( F |` W ) : W -1-1-> U /\ ( ( M ` R ) e. W /\ ( N ` R ) e. W ) ) -> ( ( ( F |` W ) ` ( M ` R ) ) = ( ( F |` W ) ` ( N ` R ) ) <-> ( M ` R ) = ( N ` R ) ) )
150 148 42 140 149 syl12anc 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( ( ( F |` W ) ` ( M ` R ) ) = ( ( F |` W ) ` ( N ` R ) ) <-> ( M ` R ) = ( N ` R ) ) )
151 143 150 mpbid 
 |-  ( ( ( ph /\ ps ) /\ ( M ` Q ) = ( N ` Q ) ) -> ( M ` R ) = ( N ` R ) )
152 151 ex 
 |-  ( ( ph /\ ps ) -> ( ( M ` Q ) = ( N ` Q ) -> ( M ` R ) = ( N ` R ) ) )
153 129 simprbda 
 |-  ( ( ph /\ Q e. ( `' M " W ) ) -> Q e. Y )
154 127 153 syldan 
 |-  ( ( ph /\ ps ) -> Q e. Y )
155 fveq2 
 |-  ( x = Q -> ( M ` x ) = ( M ` Q ) )
156 fveq2 
 |-  ( x = Q -> ( N ` x ) = ( N ` Q ) )
157 155 156 eqeq12d 
 |-  ( x = Q -> ( ( M ` x ) = ( N ` x ) <-> ( M ` Q ) = ( N ` Q ) ) )
158 157 elrab3 
 |-  ( Q e. Y -> ( Q e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( M ` Q ) = ( N ` Q ) ) )
159 154 158 syl 
 |-  ( ( ph /\ ps ) -> ( Q e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( M ` Q ) = ( N ` Q ) ) )
160 fveq2 
 |-  ( x = R -> ( M ` x ) = ( M ` R ) )
161 fveq2 
 |-  ( x = R -> ( N ` x ) = ( N ` R ) )
162 160 161 eqeq12d 
 |-  ( x = R -> ( ( M ` x ) = ( N ` x ) <-> ( M ` R ) = ( N ` R ) ) )
163 162 elrab3 
 |-  ( R e. Y -> ( R e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( M ` R ) = ( N ` R ) ) )
164 29 163 syl 
 |-  ( ( ph /\ ps ) -> ( R e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( M ` R ) = ( N ` R ) ) )
165 152 159 164 3imtr4d 
 |-  ( ( ph /\ ps ) -> ( Q e. { x e. Y | ( M ` x ) = ( N ` x ) } -> R e. { x e. Y | ( M ` x ) = ( N ` x ) } ) )
166 34 ffnd 
 |-  ( ph -> N Fn Y )
167 fndmin 
 |-  ( ( M Fn Y /\ N Fn Y ) -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
168 25 166 167 syl2anc 
 |-  ( ph -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
169 168 adantr 
 |-  ( ( ph /\ ps ) -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
170 169 eleq2d 
 |-  ( ( ph /\ ps ) -> ( Q e. dom ( M i^i N ) <-> Q e. { x e. Y | ( M ` x ) = ( N ` x ) } ) )
171 169 eleq2d 
 |-  ( ( ph /\ ps ) -> ( R e. dom ( M i^i N ) <-> R e. { x e. Y | ( M ` x ) = ( N ` x ) } ) )
172 165 170 171 3imtr4d 
 |-  ( ( ph /\ ps ) -> ( Q e. dom ( M i^i N ) -> R e. dom ( M i^i N ) ) )