Metamath Proof Explorer


Theorem cvmliftmolem1

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

Ref Expression
Hypotheses cvmliftmo.b 𝐵 = 𝐶
cvmliftmo.y 𝑌 = 𝐾
cvmliftmo.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftmo.k ( 𝜑𝐾 ∈ Conn )
cvmliftmo.l ( 𝜑𝐾 ∈ 𝑛-Locally Conn )
cvmliftmo.o ( 𝜑𝑂𝑌 )
cvmliftmoi.m ( 𝜑𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
cvmliftmoi.n ( 𝜑𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
cvmliftmoi.g ( 𝜑 → ( 𝐹𝑀 ) = ( 𝐹𝑁 ) )
cvmliftmoi.p ( 𝜑 → ( 𝑀𝑂 ) = ( 𝑁𝑂 ) )
cvmliftmolem.1 𝑆 = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
cvmliftmolem.2 ( ( 𝜑𝜓 ) → 𝑇 ∈ ( 𝑆𝑈 ) )
cvmliftmolem.3 ( ( 𝜑𝜓 ) → 𝑊𝑇 )
cvmliftmolem.4 ( ( 𝜑𝜓 ) → 𝐼 ⊆ ( 𝑀𝑊 ) )
cvmliftmolem.5 ( ( 𝜑𝜓 ) → ( 𝐾t 𝐼 ) ∈ Conn )
cvmliftmolem.6 ( ( 𝜑𝜓 ) → 𝑋𝐼 )
cvmliftmolem.7 ( ( 𝜑𝜓 ) → 𝑄𝐼 )
cvmliftmolem.8 ( ( 𝜑𝜓 ) → 𝑅𝐼 )
cvmliftmolem.9 ( ( 𝜑𝜓 ) → ( 𝐹 ‘ ( 𝑀𝑋 ) ) ∈ 𝑈 )
Assertion cvmliftmolem1 ( ( 𝜑𝜓 ) → ( 𝑄 ∈ dom ( 𝑀𝑁 ) → 𝑅 ∈ dom ( 𝑀𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 cvmliftmo.b 𝐵 = 𝐶
2 cvmliftmo.y 𝑌 = 𝐾
3 cvmliftmo.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmliftmo.k ( 𝜑𝐾 ∈ Conn )
5 cvmliftmo.l ( 𝜑𝐾 ∈ 𝑛-Locally Conn )
6 cvmliftmo.o ( 𝜑𝑂𝑌 )
7 cvmliftmoi.m ( 𝜑𝑀 ∈ ( 𝐾 Cn 𝐶 ) )
8 cvmliftmoi.n ( 𝜑𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
9 cvmliftmoi.g ( 𝜑 → ( 𝐹𝑀 ) = ( 𝐹𝑁 ) )
10 cvmliftmoi.p ( 𝜑 → ( 𝑀𝑂 ) = ( 𝑁𝑂 ) )
11 cvmliftmolem.1 𝑆 = ( 𝑘𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( 𝑠 = ( 𝐹𝑘 ) ∧ ∀ 𝑢𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢𝑣 ) = ∅ ∧ ( 𝐹𝑢 ) ∈ ( ( 𝐶t 𝑢 ) Homeo ( 𝐽t 𝑘 ) ) ) ) } )
12 cvmliftmolem.2 ( ( 𝜑𝜓 ) → 𝑇 ∈ ( 𝑆𝑈 ) )
13 cvmliftmolem.3 ( ( 𝜑𝜓 ) → 𝑊𝑇 )
14 cvmliftmolem.4 ( ( 𝜑𝜓 ) → 𝐼 ⊆ ( 𝑀𝑊 ) )
15 cvmliftmolem.5 ( ( 𝜑𝜓 ) → ( 𝐾t 𝐼 ) ∈ Conn )
16 cvmliftmolem.6 ( ( 𝜑𝜓 ) → 𝑋𝐼 )
17 cvmliftmolem.7 ( ( 𝜑𝜓 ) → 𝑄𝐼 )
18 cvmliftmolem.8 ( ( 𝜑𝜓 ) → 𝑅𝐼 )
19 cvmliftmolem.9 ( ( 𝜑𝜓 ) → ( 𝐹 ‘ ( 𝑀𝑋 ) ) ∈ 𝑈 )
20 9 adantr ( ( 𝜑𝜓 ) → ( 𝐹𝑀 ) = ( 𝐹𝑁 ) )
21 20 fveq1d ( ( 𝜑𝜓 ) → ( ( 𝐹𝑀 ) ‘ 𝑅 ) = ( ( 𝐹𝑁 ) ‘ 𝑅 ) )
22 14 18 sseldd ( ( 𝜑𝜓 ) → 𝑅 ∈ ( 𝑀𝑊 ) )
23 2 1 cnf ( 𝑀 ∈ ( 𝐾 Cn 𝐶 ) → 𝑀 : 𝑌𝐵 )
24 7 23 syl ( 𝜑𝑀 : 𝑌𝐵 )
25 24 ffnd ( 𝜑𝑀 Fn 𝑌 )
26 elpreima ( 𝑀 Fn 𝑌 → ( 𝑅 ∈ ( 𝑀𝑊 ) ↔ ( 𝑅𝑌 ∧ ( 𝑀𝑅 ) ∈ 𝑊 ) ) )
27 25 26 syl ( 𝜑 → ( 𝑅 ∈ ( 𝑀𝑊 ) ↔ ( 𝑅𝑌 ∧ ( 𝑀𝑅 ) ∈ 𝑊 ) ) )
28 27 simprbda ( ( 𝜑𝑅 ∈ ( 𝑀𝑊 ) ) → 𝑅𝑌 )
29 22 28 syldan ( ( 𝜑𝜓 ) → 𝑅𝑌 )
30 fvco3 ( ( 𝑀 : 𝑌𝐵𝑅𝑌 ) → ( ( 𝐹𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀𝑅 ) ) )
31 24 30 sylan ( ( 𝜑𝑅𝑌 ) → ( ( 𝐹𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀𝑅 ) ) )
32 29 31 syldan ( ( 𝜑𝜓 ) → ( ( 𝐹𝑀 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑀𝑅 ) ) )
33 2 1 cnf ( 𝑁 ∈ ( 𝐾 Cn 𝐶 ) → 𝑁 : 𝑌𝐵 )
34 8 33 syl ( 𝜑𝑁 : 𝑌𝐵 )
35 fvco3 ( ( 𝑁 : 𝑌𝐵𝑅𝑌 ) → ( ( 𝐹𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
36 34 35 sylan ( ( 𝜑𝑅𝑌 ) → ( ( 𝐹𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
37 29 36 syldan ( ( 𝜑𝜓 ) → ( ( 𝐹𝑁 ) ‘ 𝑅 ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
38 21 32 37 3eqtr3d ( ( 𝜑𝜓 ) → ( 𝐹 ‘ ( 𝑀𝑅 ) ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
39 38 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝐹 ‘ ( 𝑀𝑅 ) ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
40 27 simplbda ( ( 𝜑𝑅 ∈ ( 𝑀𝑊 ) ) → ( 𝑀𝑅 ) ∈ 𝑊 )
41 22 40 syldan ( ( 𝜑𝜓 ) → ( 𝑀𝑅 ) ∈ 𝑊 )
42 41 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑀𝑅 ) ∈ 𝑊 )
43 fvres ( ( 𝑀𝑅 ) ∈ 𝑊 → ( ( 𝐹𝑊 ) ‘ ( 𝑀𝑅 ) ) = ( 𝐹 ‘ ( 𝑀𝑅 ) ) )
44 42 43 syl ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝐹𝑊 ) ‘ ( 𝑀𝑅 ) ) = ( 𝐹 ‘ ( 𝑀𝑅 ) ) )
45 18 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝑅𝐼 )
46 fvres ( 𝑅𝐼 → ( ( 𝑁𝐼 ) ‘ 𝑅 ) = ( 𝑁𝑅 ) )
47 45 46 syl ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝑁𝐼 ) ‘ 𝑅 ) = ( 𝑁𝑅 ) )
48 eqid ( 𝐾t 𝐼 ) = ( 𝐾t 𝐼 )
49 15 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝐾t 𝐼 ) ∈ Conn )
50 8 adantr ( ( 𝜑𝜓 ) → 𝑁 ∈ ( 𝐾 Cn 𝐶 ) )
51 cnvimass ( 𝑀𝑊 ) ⊆ dom 𝑀
52 51 24 fssdm ( 𝜑 → ( 𝑀𝑊 ) ⊆ 𝑌 )
53 52 adantr ( ( 𝜑𝜓 ) → ( 𝑀𝑊 ) ⊆ 𝑌 )
54 14 53 sstrd ( ( 𝜑𝜓 ) → 𝐼𝑌 )
55 2 cnrest ( ( 𝑁 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝐼𝑌 ) → ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn 𝐶 ) )
56 50 54 55 syl2anc ( ( 𝜑𝜓 ) → ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn 𝐶 ) )
57 3 adantr ( ( 𝜑𝜓 ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
58 cvmtop1 ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
59 57 58 syl ( ( 𝜑𝜓 ) → 𝐶 ∈ Top )
60 1 toptopon ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
61 59 60 sylib ( ( 𝜑𝜓 ) → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
62 df-ima ( 𝑁𝐼 ) = ran ( 𝑁𝐼 )
63 elssuni ( 𝑊𝑇𝑊 𝑇 )
64 13 63 syl ( ( 𝜑𝜓 ) → 𝑊 𝑇 )
65 11 cvmsuni ( 𝑇 ∈ ( 𝑆𝑈 ) → 𝑇 = ( 𝐹𝑈 ) )
66 12 65 syl ( ( 𝜑𝜓 ) → 𝑇 = ( 𝐹𝑈 ) )
67 64 66 sseqtrd ( ( 𝜑𝜓 ) → 𝑊 ⊆ ( 𝐹𝑈 ) )
68 imass2 ( 𝑊 ⊆ ( 𝐹𝑈 ) → ( 𝑀𝑊 ) ⊆ ( 𝑀 “ ( 𝐹𝑈 ) ) )
69 67 68 syl ( ( 𝜑𝜓 ) → ( 𝑀𝑊 ) ⊆ ( 𝑀 “ ( 𝐹𝑈 ) ) )
70 14 69 sstrd ( ( 𝜑𝜓 ) → 𝐼 ⊆ ( 𝑀 “ ( 𝐹𝑈 ) ) )
71 20 cnveqd ( ( 𝜑𝜓 ) → ( 𝐹𝑀 ) = ( 𝐹𝑁 ) )
72 cnvco ( 𝐹𝑀 ) = ( 𝑀 𝐹 )
73 cnvco ( 𝐹𝑁 ) = ( 𝑁 𝐹 )
74 71 72 73 3eqtr3g ( ( 𝜑𝜓 ) → ( 𝑀 𝐹 ) = ( 𝑁 𝐹 ) )
75 74 imaeq1d ( ( 𝜑𝜓 ) → ( ( 𝑀 𝐹 ) “ 𝑈 ) = ( ( 𝑁 𝐹 ) “ 𝑈 ) )
76 imaco ( ( 𝑀 𝐹 ) “ 𝑈 ) = ( 𝑀 “ ( 𝐹𝑈 ) )
77 imaco ( ( 𝑁 𝐹 ) “ 𝑈 ) = ( 𝑁 “ ( 𝐹𝑈 ) )
78 75 76 77 3eqtr3g ( ( 𝜑𝜓 ) → ( 𝑀 “ ( 𝐹𝑈 ) ) = ( 𝑁 “ ( 𝐹𝑈 ) ) )
79 70 78 sseqtrd ( ( 𝜑𝜓 ) → 𝐼 ⊆ ( 𝑁 “ ( 𝐹𝑈 ) ) )
80 34 adantr ( ( 𝜑𝜓 ) → 𝑁 : 𝑌𝐵 )
81 80 ffund ( ( 𝜑𝜓 ) → Fun 𝑁 )
82 80 fdmd ( ( 𝜑𝜓 ) → dom 𝑁 = 𝑌 )
83 54 82 sseqtrrd ( ( 𝜑𝜓 ) → 𝐼 ⊆ dom 𝑁 )
84 funimass3 ( ( Fun 𝑁𝐼 ⊆ dom 𝑁 ) → ( ( 𝑁𝐼 ) ⊆ ( 𝐹𝑈 ) ↔ 𝐼 ⊆ ( 𝑁 “ ( 𝐹𝑈 ) ) ) )
85 81 83 84 syl2anc ( ( 𝜑𝜓 ) → ( ( 𝑁𝐼 ) ⊆ ( 𝐹𝑈 ) ↔ 𝐼 ⊆ ( 𝑁 “ ( 𝐹𝑈 ) ) ) )
86 79 85 mpbird ( ( 𝜑𝜓 ) → ( 𝑁𝐼 ) ⊆ ( 𝐹𝑈 ) )
87 62 86 eqsstrrid ( ( 𝜑𝜓 ) → ran ( 𝑁𝐼 ) ⊆ ( 𝐹𝑈 ) )
88 cnvimass ( 𝐹𝑈 ) ⊆ dom 𝐹
89 cvmcn ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
90 3 89 syl ( 𝜑𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
91 eqid 𝐽 = 𝐽
92 1 91 cnf ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 𝐽 )
93 90 92 syl ( 𝜑𝐹 : 𝐵 𝐽 )
94 93 fdmd ( 𝜑 → dom 𝐹 = 𝐵 )
95 94 adantr ( ( 𝜑𝜓 ) → dom 𝐹 = 𝐵 )
96 88 95 sseqtrid ( ( 𝜑𝜓 ) → ( 𝐹𝑈 ) ⊆ 𝐵 )
97 cnrest2 ( ( 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝑁𝐼 ) ⊆ ( 𝐹𝑈 ) ∧ ( 𝐹𝑈 ) ⊆ 𝐵 ) → ( ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn 𝐶 ) ↔ ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn ( 𝐶t ( 𝐹𝑈 ) ) ) ) )
98 61 87 96 97 syl3anc ( ( 𝜑𝜓 ) → ( ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn 𝐶 ) ↔ ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn ( 𝐶t ( 𝐹𝑈 ) ) ) ) )
99 56 98 mpbid ( ( 𝜑𝜓 ) → ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn ( 𝐶t ( 𝐹𝑈 ) ) ) )
100 99 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑁𝐼 ) ∈ ( ( 𝐾t 𝐼 ) Cn ( 𝐶t ( 𝐹𝑈 ) ) ) )
101 df-ss ( 𝑊 ⊆ ( 𝐹𝑈 ) ↔ ( 𝑊 ∩ ( 𝐹𝑈 ) ) = 𝑊 )
102 67 101 sylib ( ( 𝜑𝜓 ) → ( 𝑊 ∩ ( 𝐹𝑈 ) ) = 𝑊 )
103 1 topopn ( 𝐶 ∈ Top → 𝐵𝐶 )
104 59 103 syl ( ( 𝜑𝜓 ) → 𝐵𝐶 )
105 104 96 ssexd ( ( 𝜑𝜓 ) → ( 𝐹𝑈 ) ∈ V )
106 11 cvmsss ( 𝑇 ∈ ( 𝑆𝑈 ) → 𝑇𝐶 )
107 12 106 syl ( ( 𝜑𝜓 ) → 𝑇𝐶 )
108 107 13 sseldd ( ( 𝜑𝜓 ) → 𝑊𝐶 )
109 elrestr ( ( 𝐶 ∈ Top ∧ ( 𝐹𝑈 ) ∈ V ∧ 𝑊𝐶 ) → ( 𝑊 ∩ ( 𝐹𝑈 ) ) ∈ ( 𝐶t ( 𝐹𝑈 ) ) )
110 59 105 108 109 syl3anc ( ( 𝜑𝜓 ) → ( 𝑊 ∩ ( 𝐹𝑈 ) ) ∈ ( 𝐶t ( 𝐹𝑈 ) ) )
111 102 110 eqeltrrd ( ( 𝜑𝜓 ) → 𝑊 ∈ ( 𝐶t ( 𝐹𝑈 ) ) )
112 111 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝑊 ∈ ( 𝐶t ( 𝐹𝑈 ) ) )
113 11 cvmscld ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆𝑈 ) ∧ 𝑊𝑇 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶t ( 𝐹𝑈 ) ) ) )
114 57 12 13 113 syl3anc ( ( 𝜑𝜓 ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶t ( 𝐹𝑈 ) ) ) )
115 114 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝑊 ∈ ( Clsd ‘ ( 𝐶t ( 𝐹𝑈 ) ) ) )
116 conntop ( 𝐾 ∈ Conn → 𝐾 ∈ Top )
117 4 116 syl ( 𝜑𝐾 ∈ Top )
118 117 adantr ( ( 𝜑𝜓 ) → 𝐾 ∈ Top )
119 2 restuni ( ( 𝐾 ∈ Top ∧ 𝐼𝑌 ) → 𝐼 = ( 𝐾t 𝐼 ) )
120 118 54 119 syl2anc ( ( 𝜑𝜓 ) → 𝐼 = ( 𝐾t 𝐼 ) )
121 17 120 eleqtrd ( ( 𝜑𝜓 ) → 𝑄 ( 𝐾t 𝐼 ) )
122 121 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝑄 ( 𝐾t 𝐼 ) )
123 17 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝑄𝐼 )
124 fvres ( 𝑄𝐼 → ( ( 𝑁𝐼 ) ‘ 𝑄 ) = ( 𝑁𝑄 ) )
125 123 124 syl ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝑁𝐼 ) ‘ 𝑄 ) = ( 𝑁𝑄 ) )
126 simpr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑀𝑄 ) = ( 𝑁𝑄 ) )
127 14 17 sseldd ( ( 𝜑𝜓 ) → 𝑄 ∈ ( 𝑀𝑊 ) )
128 elpreima ( 𝑀 Fn 𝑌 → ( 𝑄 ∈ ( 𝑀𝑊 ) ↔ ( 𝑄𝑌 ∧ ( 𝑀𝑄 ) ∈ 𝑊 ) ) )
129 25 128 syl ( 𝜑 → ( 𝑄 ∈ ( 𝑀𝑊 ) ↔ ( 𝑄𝑌 ∧ ( 𝑀𝑄 ) ∈ 𝑊 ) ) )
130 129 simplbda ( ( 𝜑𝑄 ∈ ( 𝑀𝑊 ) ) → ( 𝑀𝑄 ) ∈ 𝑊 )
131 127 130 syldan ( ( 𝜑𝜓 ) → ( 𝑀𝑄 ) ∈ 𝑊 )
132 131 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑀𝑄 ) ∈ 𝑊 )
133 126 132 eqeltrrd ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑁𝑄 ) ∈ 𝑊 )
134 125 133 eqeltrd ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝑁𝐼 ) ‘ 𝑄 ) ∈ 𝑊 )
135 48 49 100 112 115 122 134 conncn ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑁𝐼 ) : ( 𝐾t 𝐼 ) ⟶ 𝑊 )
136 120 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → 𝐼 = ( 𝐾t 𝐼 ) )
137 136 feq2d ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝑁𝐼 ) : 𝐼𝑊 ↔ ( 𝑁𝐼 ) : ( 𝐾t 𝐼 ) ⟶ 𝑊 ) )
138 135 137 mpbird ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑁𝐼 ) : 𝐼𝑊 )
139 138 45 ffvelrnd ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝑁𝐼 ) ‘ 𝑅 ) ∈ 𝑊 )
140 47 139 eqeltrrd ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑁𝑅 ) ∈ 𝑊 )
141 fvres ( ( 𝑁𝑅 ) ∈ 𝑊 → ( ( 𝐹𝑊 ) ‘ ( 𝑁𝑅 ) ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
142 140 141 syl ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝐹𝑊 ) ‘ ( 𝑁𝑅 ) ) = ( 𝐹 ‘ ( 𝑁𝑅 ) ) )
143 39 44 142 3eqtr4d ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( 𝐹𝑊 ) ‘ ( 𝑀𝑅 ) ) = ( ( 𝐹𝑊 ) ‘ ( 𝑁𝑅 ) ) )
144 11 cvmsf1o ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝑇 ∈ ( 𝑆𝑈 ) ∧ 𝑊𝑇 ) → ( 𝐹𝑊 ) : 𝑊1-1-onto𝑈 )
145 57 12 13 144 syl3anc ( ( 𝜑𝜓 ) → ( 𝐹𝑊 ) : 𝑊1-1-onto𝑈 )
146 f1of1 ( ( 𝐹𝑊 ) : 𝑊1-1-onto𝑈 → ( 𝐹𝑊 ) : 𝑊1-1𝑈 )
147 145 146 syl ( ( 𝜑𝜓 ) → ( 𝐹𝑊 ) : 𝑊1-1𝑈 )
148 147 adantr ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝐹𝑊 ) : 𝑊1-1𝑈 )
149 f1fveq ( ( ( 𝐹𝑊 ) : 𝑊1-1𝑈 ∧ ( ( 𝑀𝑅 ) ∈ 𝑊 ∧ ( 𝑁𝑅 ) ∈ 𝑊 ) ) → ( ( ( 𝐹𝑊 ) ‘ ( 𝑀𝑅 ) ) = ( ( 𝐹𝑊 ) ‘ ( 𝑁𝑅 ) ) ↔ ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
150 148 42 140 149 syl12anc ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( ( ( 𝐹𝑊 ) ‘ ( 𝑀𝑅 ) ) = ( ( 𝐹𝑊 ) ‘ ( 𝑁𝑅 ) ) ↔ ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
151 143 150 mpbid ( ( ( 𝜑𝜓 ) ∧ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) → ( 𝑀𝑅 ) = ( 𝑁𝑅 ) )
152 151 ex ( ( 𝜑𝜓 ) → ( ( 𝑀𝑄 ) = ( 𝑁𝑄 ) → ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
153 129 simprbda ( ( 𝜑𝑄 ∈ ( 𝑀𝑊 ) ) → 𝑄𝑌 )
154 127 153 syldan ( ( 𝜑𝜓 ) → 𝑄𝑌 )
155 fveq2 ( 𝑥 = 𝑄 → ( 𝑀𝑥 ) = ( 𝑀𝑄 ) )
156 fveq2 ( 𝑥 = 𝑄 → ( 𝑁𝑥 ) = ( 𝑁𝑄 ) )
157 155 156 eqeq12d ( 𝑥 = 𝑄 → ( ( 𝑀𝑥 ) = ( 𝑁𝑥 ) ↔ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) )
158 157 elrab3 ( 𝑄𝑌 → ( 𝑄 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ↔ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) )
159 154 158 syl ( ( 𝜑𝜓 ) → ( 𝑄 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ↔ ( 𝑀𝑄 ) = ( 𝑁𝑄 ) ) )
160 fveq2 ( 𝑥 = 𝑅 → ( 𝑀𝑥 ) = ( 𝑀𝑅 ) )
161 fveq2 ( 𝑥 = 𝑅 → ( 𝑁𝑥 ) = ( 𝑁𝑅 ) )
162 160 161 eqeq12d ( 𝑥 = 𝑅 → ( ( 𝑀𝑥 ) = ( 𝑁𝑥 ) ↔ ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
163 162 elrab3 ( 𝑅𝑌 → ( 𝑅 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ↔ ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
164 29 163 syl ( ( 𝜑𝜓 ) → ( 𝑅 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ↔ ( 𝑀𝑅 ) = ( 𝑁𝑅 ) ) )
165 152 159 164 3imtr4d ( ( 𝜑𝜓 ) → ( 𝑄 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } → 𝑅 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ) )
166 34 ffnd ( 𝜑𝑁 Fn 𝑌 )
167 fndmin ( ( 𝑀 Fn 𝑌𝑁 Fn 𝑌 ) → dom ( 𝑀𝑁 ) = { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } )
168 25 166 167 syl2anc ( 𝜑 → dom ( 𝑀𝑁 ) = { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } )
169 168 adantr ( ( 𝜑𝜓 ) → dom ( 𝑀𝑁 ) = { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } )
170 169 eleq2d ( ( 𝜑𝜓 ) → ( 𝑄 ∈ dom ( 𝑀𝑁 ) ↔ 𝑄 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ) )
171 169 eleq2d ( ( 𝜑𝜓 ) → ( 𝑅 ∈ dom ( 𝑀𝑁 ) ↔ 𝑅 ∈ { 𝑥𝑌 ∣ ( 𝑀𝑥 ) = ( 𝑁𝑥 ) } ) )
172 165 170 171 3imtr4d ( ( 𝜑𝜓 ) → ( 𝑄 ∈ dom ( 𝑀𝑁 ) → 𝑅 ∈ dom ( 𝑀𝑁 ) ) )