Theorem cvmliftmolem2 31264

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

Hypotheses

Ref	Expression
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. 𝑛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

Ref	Expression
cvmliftmolem2	|- ( ph -> M = N )

Distinct variable groups:   k, s, u, v, C   k, J, s, u, v   v, B   K, s   k, M, s, u, v   N, s   ph, s   k, F, s, u, v   S, s   Y, s

Allowed substitution hints:   ph( v, u, k)   B( u, k, s)   S( v, u, k)   K( v, u, k)   N( v, u, k)   O( v, u, k, s)   Y( v, u, k)

Proof of Theorem cvmliftmolem2

Dummy variables a b t y z x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftmoi.m	. . 3 |- ( ph -> M e. ( K Cn C ) )
2		cvmliftmo.y	. . . 4 |- Y = U. K
3		cvmliftmo.b	. . . 4 |- B = U. C
4	2, 3	cnf 21050	. . 3 |- ( M e. ( K Cn C ) -> M : Y --> B )
5		ffn 6045	. . 3 |- ( M : Y --> B -> M Fn Y )
6	1, 4, 5	3syl 18	. 2 |- ( ph -> M Fn Y )
7		cvmliftmoi.n	. . 3 |- ( ph -> N e. ( K Cn C ) )
8	2, 3	cnf 21050	. . 3 |- ( N e. ( K Cn C ) -> N : Y --> B )
9		ffn 6045	. . 3 |- ( N : Y --> B -> N Fn Y )
10	7, 8, 9	3syl 18	. 2 |- ( ph -> N Fn Y )
11		cvmliftmo.k	. . . . . 6 |- ( ph -> K e. Conn )
12		inss1 3833	. . . . . . 7 |- ( K i^i ( Clsd ` K ) ) C_ K
13		cvmliftmo.f	. . . . . . . . . . . 12 |- ( ph -> F e. ( C CovMap J ) )
14	13	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ x e. Y ) -> F e. ( C CovMap J ) )
15	1, 4	syl 17	. . . . . . . . . . . . 13 |- ( ph -> M : Y --> B )
16	15	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ph /\ x e. Y ) -> ( M ` x ) e. B )
17		cvmcn 31244	. . . . . . . . . . . . . 14 |- ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
18		eqid 2622	. . . . . . . . . . . . . . 15 |- U. J = U. J
19	3, 18	cnf 21050	. . . . . . . . . . . . . 14 |- ( F e. ( C Cn J ) -> F : B --> U. J )
20	13, 17, 19	3syl 18	. . . . . . . . . . . . 13 |- ( ph -> F : B --> U. J )
21	20	ffvelrnda 6359	. . . . . . . . . . . 12 |- ( ( ph /\ ( M ` x ) e. B ) -> ( F ` ( M ` x ) ) e. U. J )
22	16, 21	syldan 487	. . . . . . . . . . 11 |- ( ( ph /\ x e. Y ) -> ( F ` ( M ` x ) ) e. U. J )
23		cvmliftmolem.1	. . . . . . . . . . . 12 |- 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 ) ) ) ) } )
24	23, 18	cvmcov 31245	. . . . . . . . . . 11 |- ( ( F e. ( C CovMap J ) /\ ( F ` ( M ` x ) ) e. U. J ) -> E. a e. J ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) )
25	14, 22, 24	syl2anc 693	. . . . . . . . . 10 |- ( ( ph /\ x e. Y ) -> E. a e. J ( ( F ` ( M ` x ) ) e. a /\ ( S ` a ) =/= (/) ) )
26		n0 3931	. . . . . . . . . . . . . 14 |- ( ( S ` a ) =/= (/) <-> E. t t e. ( S ` a ) )
27		cvmliftmo.l	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> K e. 𝑛Locally Conn )
28	27	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> K e. 𝑛Locally Conn )
29	1	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> M e. ( K Cn C ) )
30		simprrr 805	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> t e. ( S ` a ) )
31	23	cvmsss 31249	. . . . . . . . . . . . . . . . . . . . . 22 |- ( t e. ( S ` a ) -> t C_ C )
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> t C_ C )
33	13	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> F e. ( C CovMap J ) )
34	15	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> M : Y --> B )
35		simprll 802	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> x e. Y )
36	34, 35	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( M ` x ) e. B )
37		simprrl 804	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( ( x e. Y /\ a e. J ) /\ ( ( F ` ( M ` x ) ) e. a /\ t e. ( S ` a ) ) ) ) -> ( F ` ( M ` x ) ) e. a )
38		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( iota_ b e. t ( M ` x ) e. b ) = ( iota_ b e. t ( M ` x ) e. b )
39	23, 3, 38	cvmsiota 31259	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 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 ) ) )
40	33, 30, 36, 37, 39	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) )
41	40	simpld 475	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 )
42	32, 41	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 )
43		cnima 21069	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 )
44	29, 42, 43	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 )
45	40	simprd 479	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) )
46		elpreima 6337	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) ) )
47	34, 5, 46	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) ) )
48	35, 45, 47	mpbir2and 957	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) )
49		nlly2i 21279	. . . . . . . . . . . . . . . . . . 19 |- ( ( K e. 𝑛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 ) )
50	28, 44, 48, 49	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) )
51		simprr1 1109	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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 )
52		cvmliftmo.o	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> O e. Y )
53		cvmliftmoi.g	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( F o. M ) = ( F o. N ) )
54		cvmliftmoi.p	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> ( M ` O ) = ( N ` O ) )
55		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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	41	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( 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 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 1104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 1109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( 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 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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 805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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	37	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( 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	3, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 68, 70, 71	cvmliftmolem1 31263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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	3, 2, 13, 11, 27, 52, 1, 7, 53, 54, 23, 56, 57, 60, 62, 68, 70, 68, 71	cvmliftmolem1 31263	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( 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 202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 680	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 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 680	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 2966	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( 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	51, 77	jca 554	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( 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 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 680	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 3017	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 3031	. . . . . . . . . . . . . . . . . 18 |- ( ( 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	50, 82	mpd 15	. . . . . . . . . . . . . . . . 17 |- ( ( 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 680	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 643	. . . . . . . . . . . . . . 15 |- ( ( ( 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 1861	. . . . . . . . . . . . . 14 |- ( ( ( 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	26, 86	syl5bi 232	. . . . . . . . . . . . 13 |- ( ( ( 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 629	. . . . . . . . . . . 12 |- ( ( 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 680	. . . . . . . . . . 11 |- ( ( ( 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 3031	. . . . . . . . . 10 |- ( ( 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	25, 90	mpd 15	. . . . . . . . 9 |- ( ( 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 2966	. . . . . . . 8 |- ( 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 21220	. . . . . . . . . 10 |- ( K e. Conn -> K e. Top )
94	11, 93	syl 17	. . . . . . . . 9 |- ( ph -> K e. Top )
95		fndmin 6324	. . . . . . . . . . 11 |- ( ( M Fn Y /\ N Fn Y ) -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
96	6, 10, 95	syl2anc 693	. . . . . . . . . 10 |- ( ph -> dom ( M i^i N ) = { x e. Y | ( M ` x ) = ( N ` x ) } )
97		ssrab2 3687	. . . . . . . . . 10 |- { x e. Y | ( M ` x ) = ( N ` x ) } C_ Y
98	96, 97	syl6eqss 3655	. . . . . . . . 9 |- ( ph -> dom ( M i^i N ) C_ Y )
99	2	isclo 20891	. . . . . . . . 9 |- ( ( 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 693	. . . . . . . 8 |- ( 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 247	. . . . . . 7 |- ( ph -> dom ( M i^i N ) e. ( K i^i ( Clsd ` K ) ) )
102	12, 101	sseldi 3601	. . . . . 6 |- ( ph -> dom ( M i^i N ) e. K )
103		fveq2 6191	. . . . . . . . . . 11 |- ( x = O -> ( M ` x ) = ( M ` O ) )
104		fveq2 6191	. . . . . . . . . . 11 |- ( x = O -> ( N ` x ) = ( N ` O ) )
105	103, 104	eqeq12d 2637	. . . . . . . . . 10 |- ( x = O -> ( ( M ` x ) = ( N ` x ) <-> ( M ` O ) = ( N ` O ) ) )
106	105	elrab 3363	. . . . . . . . 9 |- ( O e. { x e. Y | ( M ` x ) = ( N ` x ) } <-> ( O e. Y /\ ( M ` O ) = ( N ` O ) ) )
107	52, 54, 106	sylanbrc 698	. . . . . . . 8 |- ( ph -> O e. { x e. Y | ( M ` x ) = ( N ` x ) } )
108	107, 96	eleqtrrd 2704	. . . . . . 7 |- ( ph -> O e. dom ( M i^i N ) )
109		ne0i 3921	. . . . . . 7 |- ( O e. dom ( M i^i N ) -> dom ( M i^i N ) =/= (/) )
110	108, 109	syl 17	. . . . . 6 |- ( ph -> dom ( M i^i N ) =/= (/) )
111		inss2 3834	. . . . . . 7 |- ( K i^i ( Clsd ` K ) ) C_ ( Clsd ` K )
112	111, 101	sseldi 3601	. . . . . 6 |- ( ph -> dom ( M i^i N ) e. ( Clsd ` K ) )
113	2, 11, 102, 110, 112	connclo 21218	. . . . 5 |- ( ph -> dom ( M i^i N ) = Y )
114	113, 96	eqtr3d 2658	. . . 4 |- ( ph -> Y = { x e. Y | ( M ` x ) = ( N ` x ) } )
115		rabid2 3118	. . . 4 |- ( Y = { x e. Y | ( M ` x ) = ( N ` x ) } <-> A. x e. Y ( M ` x ) = ( N ` x ) )
116	114, 115	sylib 208	. . 3 |- ( ph -> A. x e. Y ( M ` x ) = ( N ` x ) )
117	116	r19.21bi 2932	. 2 |- ( ( ph /\ x e. Y ) -> ( M ` x ) = ( N ` x ) )
118	6, 10, 117	eqfnfvd 6314	1 |- ( ph -> M = N )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   \ cdif 3571   i^i cin 3573   C_ wss 3574   (/)c0 3915   ~Pcpw 4158   {csn 4177   U.cuni 4436   |-> cmpt 4729   `'ccnv 5113   dom cdm 5114   |` cres 5116   "cima 5117   o. ccom 5118   Fn wfn 5883   -->wf 5884   ` cfv 5888   iota_crio 6610  (class class class)co 6650   ↾_t crest 16081   Topctop 20698   Clsdccld 20820   Cn ccn 21028  Conncconn 21214  𝑛Locally cnlly 21268   Homeochmeo 21556   CovMap ccvm 31237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-nei 20902  df-cn 21031  df-conn 21215  df-nlly 21270  df-hmeo 21558  df-cvm 31238

This theorem is referenced by:  cvmliftmoi  31265