Metamath Proof Explorer

Theorem cvmliftlem6

Description: Lemma for cvmlift . Induction step for cvmliftlem7 . Assuming that Q ( M - 1 ) is defined at ( M - 1 ) / N and is a preimage of G ( ( M - 1 ) / N ) , the next segment Q ( M ) is also defined and is a function on W which is a lift G for this segment. This follows explicitly from the definition Q ( M ) =`' ( F |`I ) o. G since G is in 1st( FM ) for the entire interval so that ` ``' ( F |`I ) maps this into I and F o. Q maps back to G . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
cvmliftlem5.3 ⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
cvmliftlem6.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
cvmliftlem6.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
Assertion cvmliftlem6 ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑄 ‘ 𝑀 ) : 𝑊 ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 𝑀 ) ) = ( 𝐺 ↾ 𝑊 ) ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
3 cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
4 cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
6 cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
7 cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
8 cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
10 cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
11 cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
12 cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
13 cvmliftlem5.3 ⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
14 cvmliftlem6.1 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
15 cvmliftlem6.2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
16 14 adantrr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
17 1 2 3 4 5 6 7 8 9 10 11 16 cvmliftlem1 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
18 1 cvmsss ⊢ ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ 𝐶 )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ 𝐶 )
20 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
21 15 adantrr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
22 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
23 2 3 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
24 20 22 23 3syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝐹 : 𝐵 ⟶ 𝑋 )
25 ffn ⊢ ( 𝐹 : 𝐵 ⟶ 𝑋 → 𝐹 Fn 𝐵 )
26 fniniseg ⊢ ( 𝐹 Fn 𝐵 → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
27 24 25 26 3syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
28 21 27 mpbid ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
29 28 simpld ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 )
30 28 simprd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
31 elfznn ⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ∈ ℕ )
32 16 31 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑀 ∈ ℕ )
33 32 nnred ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑀 ∈ ℝ )
34 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
35 33 34 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
36 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑁 ∈ ℕ )
37 35 36 nndivred ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ )
38 37 rexrd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* )
39 33 36 nndivred ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
40 39 rexrd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ* )
41 33 ltm1d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝑀 − 1 ) < 𝑀 )
42 36 nnred ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑁 ∈ ℝ )
43 36 nngt0d ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 0 < 𝑁 )
44 ltdiv1 ⊢ ( ( ( 𝑀 − 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
45 35 33 42 43 44 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
46 41 45 mpbid ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) )
47 37 39 46 ltled ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) )
48 lbicc2 ⊢ ( ( ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑀 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
49 38 40 47 48 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
50 49 13 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ 𝑊 )
51 1 2 3 4 5 6 7 8 9 10 11 16 13 50 cvmliftlem3 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
52 30 51 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
53 eqid ⊢ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 )
54 1 2 53 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
55 20 17 29 52 54 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
56 55 simpld ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) )
57 19 56 sseldd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ 𝐶 )
58 elssuni ⊢ ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ 𝐶 → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ⊆ ∪ 𝐶 )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ⊆ ∪ 𝐶 )
60 59 2 sseqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ⊆ 𝐵 )
61 1 cvmsf1o ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
62 20 17 56 61 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
63 f1ocnv ⊢ ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) –1-1-onto→ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
64 f1of ⊢ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) –1-1-onto→ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⟶ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
65 62 63 64 3syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⟶ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
66 simprr ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → 𝑧 ∈ 𝑊 )
67 1 2 3 4 5 6 7 8 9 10 11 16 13 66 cvmliftlem3 ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
68 65 67 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
69 60 68 sseldd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐵 )
70 69 anassrs ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑧 ∈ 𝑊 ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ 𝐵 )
71 70 fmpttd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) : 𝑊 ⟶ 𝐵 )
72 14 31 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℕ )
73 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem5 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
74 72 73 syldan ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
75 74 feq1d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑄 ‘ 𝑀 ) : 𝑊 ⟶ 𝐵 ↔ ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) : 𝑊 ⟶ 𝐵 ) )
76 71 75 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑄 ‘ 𝑀 ) : 𝑊 ⟶ 𝐵 )
77 fvres ⊢ ( 𝑧 ∈ 𝑊 → ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
78 66 77 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
79 f1ocnvfv2 ⊢ ( ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) : ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) –1-1-onto→ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝐺 ‘ 𝑧 ) )
80 62 67 79 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝐺 ‘ 𝑧 ) )
81 fvres ⊢ ( ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
82 68 81 syl ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
83 78 80 82 3eqtr2rd ⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) )
84 83 anassrs ⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝑧 ∈ 𝑊 ) → ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) )
85 84 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑧 ∈ 𝑊 ↦ ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ 𝑊 ↦ ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) ) )
86 4 22 23 3syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝑋 )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
88 87 feqmptd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐹 = ( 𝑦 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑦 ) ) )
89 fveq2 ⊢ ( 𝑦 = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
90 70 74 88 89 fmptco ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ∘ ( 𝑄 ‘ 𝑀 ) ) = ( 𝑧 ∈ 𝑊 ↦ ( 𝐹 ‘ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) )
91 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
92 91 3 cnf ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
93 5 92 syl ⊢ ( 𝜑 → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
95 1 2 3 4 5 6 7 8 9 10 11 14 13 cvmliftlem2 ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑊 ⊆ ( 0 [,] 1 ) )
96 94 95 fssresd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ↾ 𝑊 ) : 𝑊 ⟶ 𝑋 )
97 96 feqmptd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐺 ↾ 𝑊 ) = ( 𝑧 ∈ 𝑊 ↦ ( ( 𝐺 ↾ 𝑊 ) ‘ 𝑧 ) ) )
98 85 90 97 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐹 ∘ ( 𝑄 ‘ 𝑀 ) ) = ( 𝐺 ↾ 𝑊 ) )
99 76 98 jca ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑄 ‘ 𝑀 ) : 𝑊 ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 𝑀 ) ) = ( 𝐺 ↾ 𝑊 ) ) )