Metamath Proof Explorer

Theorem cvmliftmolem2

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 ) ) ) ) } )
Assertion cvmliftmolem2 
|- ( ph -> M = 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 2 1 cnf 
 |-  ( M e. ( K Cn C ) -> M : Y --> B )
13 ffn 
 |-  ( M : Y --> B -> M Fn Y )
14 7 12 13 3syl 
 |-  ( ph -> M Fn Y )
15 2 1 cnf 
 |-  ( N e. ( K Cn C ) -> N : Y --> B )
16 ffn 
 |-  ( N : Y --> B -> N Fn Y )
17 8 15 16 3syl 
 |-  ( ph -> N Fn Y )
18 inss1 
 |-  ( K i^i ( Clsd ` K ) ) C_ K
19 3 adantr 
 |-  ( ( ph /\ x e. Y ) -> F e. ( C CovMap J ) )
20 7 12 syl 
 |-  ( ph -> M : Y --> B )
21 20 ffvelrnda 
 |-  ( ( ph /\ x e. Y ) -> ( M ` x ) e. B )
22 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
23 eqid 
 |-  U. J = U. J
24 1 23 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
25 3 22 24 3syl 
 |-  ( ph -> F : B --> U. J )
26 25 ffvelrnda 
 |-  ( ( ph /\ ( M ` x ) e. B ) -> ( F ` ( M ` x ) ) e. U. J )
27 21 26 syldan 
 |-  ( ( ph /\ x e. Y ) -> ( F ` ( M ` x ) ) e. U. J )
28 11 23 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ ( F ` ( M ` x ) ) e. U. J ) -> E. a e. J ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) )
29 19 27 28 syl2anc 
 |-  ( ( ph /\ x e. Y ) -> E. a e. J ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) )
30 n0 
 |-  ( ( S ` a ) =/= (/) <-> E. t t e. ( S ` a ) )
31 5 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> K e. N-Locally Conn )
32 7 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> M e. ( K Cn C ) )
33 simprrr 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> t e. ( S ` a ) )
34 11 cvmsss 
 |-  ( t e. ( S ` a ) -> t C_ C )
35 33 34 syl 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> t C_ C )
36 3 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> F e. ( C CovMap J ) )
37 20 adantr 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> M : Y --> B )
38 simprll 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> x e. Y )
39 37 38 ffvelrnd 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( M ` x ) e. B )
40 simprrl 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( F ` ( M ` x ) ) e. a )
41 eqid 
 |-  ( iota_ b e. t ( M ` x ) e. b ) = ( iota_ b e. t ( M ` x ) e. b )
42 11 1 41 cvmsiota 
 |-  ( ( F e. ( C CovMap J ) /\ ( t e. ( S ` a ) /\ ( M ` x ) e. B /\ ( F ` ( M ` x ) ) e. a ) ) -> ( ( iota_ b e. t ( M ` x ) e. b ) e. t /\ ( M ` x ) e. ( iota_ b e. t ( M ` x ) e. b ) ) )
43 36 33 39 40 42 syl13anc 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( ( iota_ b e. t ( M ` x ) e. b ) e. t /\ ( M ` x ) e. ( iota_ b e. t ( M ` x ) e. b ) ) )
44 43 simpld 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( iota_ b e. t ( M ` x ) e. b ) e. t )
45 35 44 sseldd 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( iota_ b e. t ( M ` x ) e. b ) e. C )
46 cnima 
 |-  ( ( M e. ( K Cn C ) /\ ( iota_ b e. t ( M ` x ) e. b ) e. C ) -> ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) e. K )
47 32 45 46 syl2anc 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) e. K )
48 43 simprd 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( M ` x ) e. ( iota_ b e. t ( M ` x ) e. b ) )
49 elpreima 
 |-  ( M Fn Y -> ( x e. ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) <-> ( x e. Y /\ ( M ` x ) e. ( iota_ b e. t ( M ` x ) e. b ) ) ) )
50 37 13 49 3syl 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( x e. ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) <-> ( x e. Y /\ ( M ` x ) e. ( iota_ b e. t ( M ` x ) e. b ) ) ) )
51 38 48 50 mpbir2and 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> x e. ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) )
52 nlly2i 
 |-  ( ( K e. N-Locally Conn /\ ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) e. K /\ x e. ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) ) -> E. s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) E. y e. K ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) )
53 31 47 51 52 syl3anc 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> E. s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) E. y e. K ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) )
54 simprr1 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) -> x e. y )
55 simplrr 
 |-  ( ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) -> t e. ( S ` a ) )
56 55 adantl 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> t e. ( S ` a ) )
57 44 adantrr 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( iota_ b e. t ( M ` x ) e. b ) e. t )
58 simplll 
 |-  ( ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) -> s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) )
59 58 ad2antll 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) )
60 59 elpwid 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> s C_ ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) )
61 simplr3 
 |-  ( ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) -> ( K |`t s ) e. Conn )
62 61 ad2antll 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( K |`t s ) e. Conn )
63 simplr2 
 |-  ( ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) -> y C_ s )
64 63 ad2antll 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> y C_ s )
65 simprr1 
 |-  ( ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) -> x e. y )
66 65 adantl 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) ) -> x e. y )
67 66 adantrrr 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> x e. y )
68 64 67 sseldd 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> x e. s )
69 simprrr 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> z e. y )
70 64 69 sseldd 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> z e. s )
71 40 adantrr 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( F ` ( M ` x ) ) e. a )
72 1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 68 70 71 cvmliftmolem1 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( x e. dom ( M i^i N ) -> z e. dom ( M i^i N ) ) )
73 1 2 3 4 5 6 7 8 9 10 11 56 57 60 62 68 70 68 71 cvmliftmolem1 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( z e. dom ( M i^i N ) -> x e. dom ( M i^i N ) ) )
74 72 73 impbid 
 |-  ( ( ph /\ ( ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) ) -> ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) )
75 74 anassrs 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) /\ z e. y ) ) -> ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) )
76 75 anassrs 
 |-  ( ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) /\ z e. y ) -> ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) )
77 76 ralrimiva 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) -> A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) )
78 54 77 jca 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) /\ ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) ) ) -> ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) )
79 78 expr 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ ( s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) /\ y e. K ) ) -> ( ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) -> ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
80 79 anassrs 
 |-  ( ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) ) /\ y e. K ) -> ( ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) -> ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
81 80 reximdva 
 |-  ( ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) /\ s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) ) -> ( E. y e. K ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
82 81 rexlimdva 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( E. s e. ~P ( `' M " ( iota_ b e. t ( M ` x ) e. b ) ) E. y e. K ( x e. y /\ y C_ s /\ ( K |`t s ) e. Conn ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
83 53 82 mpd 
 |-  ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) )
84 83 anassrs 
 |-  ( ( ( ph /\ ( x e. Y /\ a e. J ) ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) )
85 84 expr 
 |-  ( ( ( ph /\ ( x e. Y /\ a e. J ) ) /\ ( F ` ( M ` x ) ) e. a ) -> ( t e. ( S ` a ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
86 85 exlimdv 
 |-  ( ( ( ph /\ ( x e. Y /\ a e. J ) ) /\ ( F ` ( M ` x ) ) e. a ) -> ( E. t t e. ( S ` a ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
87 30 86 syl5bi 
 |-  ( ( ( ph /\ ( x e. Y /\ a e. J ) ) /\ ( F ` ( M ` x ) ) e. a ) -> ( ( S ` a ) =/= (/) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
88 87 expimpd 
 |-  ( ( ph /\ ( x e. Y /\ a e. J ) ) -> ( ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
89 88 anassrs 
 |-  ( ( ( ph /\ x e. Y ) /\ a e. J ) -> ( ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
90 89 rexlimdva 
 |-  ( ( ph /\ x e. Y ) -> ( E. a e. J ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
91 29 90 mpd 
 |-  ( ( ph /\ x e. Y ) -> E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) )
92 91 ralrimiva 
 |-  ( ph -> A. x e. Y E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) )
93 conntop 
 |-  ( K e. Conn -> K e. Top )
94 4 93 syl 
 |-  ( ph -> K e. Top )
95 fndmin 
 |-  ( ( M Fn Y /\ N Fn Y ) -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
96 14 17 95 syl2anc 
 |-  ( ph -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
97 ssrab2 
 |-  { x e. Y | ( M ` x ) = ( N ` x ) } C_ Y
98 96 97 eqsstrdi 
 |-  ( ph -> dom ( M i^i N ) C_ Y )
99 2 isclo 
 |-  ( ( K e. Top /\ dom ( M i^i N ) C_ Y ) -> ( dom ( M i^i N ) e. ( K i^i ( Clsd ` K ) ) <-> A. x e. Y E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
100 94 98 99 syl2anc 
 |-  ( ph -> ( dom ( M i^i N ) e. ( K i^i ( Clsd ` K ) ) <-> A. x e. Y E. y e. K ( x e. y /\ A. z e. y ( x e. dom ( M i^i N ) <-> z e. dom ( M i^i N ) ) ) ) )
101 92 100 mpbird 
 |-  ( ph -> dom ( M i^i N ) e. ( K i^i ( Clsd ` K ) ) )
102 18 101 sseldi 
 |-  ( ph -> dom ( M i^i N ) e. K )
103 fveq2 
 |-  ( x = O -> ( M ` x ) = ( M ` O ) )
104 fveq2 
 |-  ( x = O -> ( N ` x ) = ( N ` O ) )
105 103 104 eqeq12d 
 |-  ( x = O -> ( ( M ` x ) = ( N ` x ) <-> ( M ` O ) = ( N ` O ) ) )
106 105 elrab 
 |-  ( O e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( O e. Y /\ ( M ` O ) = ( N ` O ) ) )
107 6 10 106 sylanbrc 
 |-  ( ph -> O e. { x e. Y | ( M ` x ) = ( N ` x ) } )
108 107 96 eleqtrrd 
 |-  ( ph -> O e. dom ( M i^i N ) )
109 108 ne0d 
 |-  ( ph -> dom ( M i^i N ) =/= (/) )
110 inss2 
 |-  ( K i^i ( Clsd ` K ) ) C_ ( Clsd ` K )
111 110 101 sseldi 
 |-  ( ph -> dom ( M i^i N ) e. ( Clsd ` K ) )
112 2 4 102 109 111 connclo 
 |-  ( ph -> dom ( M i^i N ) = Y )
113 112 96 eqtr3d 
 |-  ( ph -> Y = { x e. Y | ( M ` x ) = ( N ` x ) } )
114 rabid2 
 |-  ( Y = { x e. Y | ( M ` x ) = ( N ` x ) } <-> A. x e. Y ( M ` x ) = ( N ` x ) )
115 113 114 sylib 
 |-  ( ph -> A. x e. Y ( M ` x ) = ( N ` x ) )
116 115 r19.21bi 
 |-  ( ( ph /\ x e. Y ) -> ( M ` x ) = ( N ` x ) )
117 14 17 116 eqfnfvd 
 |-  ( ph -> M = N )