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 dfss2 ⊢ ( 𝑊 ⊆ ( ◡ 𝐹 “ 𝑈 ) ↔ ( 𝑊 ∩ ( ◡ 𝐹 “ 𝑈 ) ) = 𝑊 )
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 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝑀 ‘ 𝑄 ) = ( 𝑁 ‘ 𝑄 ) ) → ( ( 𝑁 ↾ 𝐼 ) ‘ 𝑅 ) ∈ 𝑊 )
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 ( 𝑀 ∩ 𝑁 ) ) )