Metamath Proof Explorer

Theorem stoweidlem31

Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in BrosowskiDeutsh p. 91: assuming that R is a finite subset of V , x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all i ranging in the finite indexing set, 0 ≤ x_i ≤ 1, x_i < ε / m on V(t_i), and x_i > 1 - ε / m on B . Here M is used to represent m in the paper, E is used to represent ε in the paper, v_i is used to represent V(t_i). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem31.1 ⊢ Ⅎ ℎ 𝜑
stoweidlem31.2 ⊢ Ⅎ 𝑡 𝜑
stoweidlem31.3 ⊢ Ⅎ 𝑤 𝜑
stoweidlem31.4 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
stoweidlem31.5 ⊢ 𝑉 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
stoweidlem31.6 ⊢ 𝐺 = ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
stoweidlem31.7 ⊢ ( 𝜑 → 𝑅 ⊆ 𝑉 )
stoweidlem31.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem31.9 ⊢ ( 𝜑 → 𝑣 : ( 1 ... 𝑀 ) –1-1-onto→ 𝑅 )
stoweidlem31.10 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem31.11 ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) )
stoweidlem31.12 ⊢ ( 𝜑 → 𝑉 ∈ V )
stoweidlem31.13 ⊢ ( 𝜑 → 𝐴 ∈ V )
stoweidlem31.14 ⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
Assertion stoweidlem31 ( 𝜑 → ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem31.1 ⊢ Ⅎ ℎ 𝜑
2 stoweidlem31.2 ⊢ Ⅎ 𝑡 𝜑
3 stoweidlem31.3 ⊢ Ⅎ 𝑤 𝜑
4 stoweidlem31.4 ⊢ 𝑌 = { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
5 stoweidlem31.5 ⊢ 𝑉 = { 𝑤 ∈ 𝐽 ∣ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) }
6 stoweidlem31.6 ⊢ 𝐺 = ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
7 stoweidlem31.7 ⊢ ( 𝜑 → 𝑅 ⊆ 𝑉 )
8 stoweidlem31.8 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
9 stoweidlem31.9 ⊢ ( 𝜑 → 𝑣 : ( 1 ... 𝑀 ) –1-1-onto→ 𝑅 )
10 stoweidlem31.10 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
11 stoweidlem31.11 ⊢ ( 𝜑 → 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) )
12 stoweidlem31.12 ⊢ ( 𝜑 → 𝑉 ∈ V )
13 stoweidlem31.13 ⊢ ( 𝜑 → 𝐴 ∈ V )
14 stoweidlem31.14 ⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
15 fnchoice ⊢ ( ran 𝐺 ∈ Fin → ∃ 𝑙 ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) )
16 14 15 syl ⊢ ( 𝜑 → ∃ 𝑙 ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) )
17 vex ⊢ 𝑙 ∈ V
18 12 7 ssexd ⊢ ( 𝜑 → 𝑅 ∈ V )
19 mptexg ⊢ ( 𝑅 ∈ V → ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ V )
20 18 19 syl ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) ∈ V )
21 6 20 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ V )
22 vex ⊢ 𝑣 ∈ V
23 coexg ⊢ ( ( 𝐺 ∈ V ∧ 𝑣 ∈ V ) → ( 𝐺 ∘ 𝑣 ) ∈ V )
24 21 22 23 sylancl ⊢ ( 𝜑 → ( 𝐺 ∘ 𝑣 ) ∈ V )
25 coexg ⊢ ( ( 𝑙 ∈ V ∧ ( 𝐺 ∘ 𝑣 ) ∈ V ) → ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ∈ V )
26 17 24 25 sylancr ⊢ ( 𝜑 → ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ∈ V )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ∈ V )
28 simprl ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → 𝑙 Fn ran 𝐺 )
29 nfcv ⊢ Ⅎ ℎ 𝑙
30 nfcv ⊢ Ⅎ ℎ 𝑅
31 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) }
32 30 31 nfmpt ⊢ Ⅎ ℎ ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
33 6 32 nfcxfr ⊢ Ⅎ ℎ 𝐺
34 33 nfrn ⊢ Ⅎ ℎ ran 𝐺
35 29 34 nffn ⊢ Ⅎ ℎ 𝑙 Fn ran 𝐺
36 nfv ⊢ Ⅎ ℎ ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
37 34 36 nfralw ⊢ Ⅎ ℎ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
38 35 37 nfan ⊢ Ⅎ ℎ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
39 1 38 nfan ⊢ Ⅎ ℎ ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) )
40 fvelrnb ⊢ ( 𝑙 Fn ran 𝐺 → ( ℎ ∈ ran 𝑙 ↔ ∃ 𝑏 ∈ ran 𝐺 ( 𝑙 ‘ 𝑏 ) = ℎ ) )
41 28 40 syl ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( ℎ ∈ ran 𝑙 ↔ ∃ 𝑏 ∈ ran 𝐺 ( 𝑙 ‘ 𝑏 ) = ℎ ) )
42 41 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ∃ 𝑏 ∈ ran 𝐺 ( 𝑙 ‘ 𝑏 ) = ℎ )
43 nfv ⊢ Ⅎ 𝑏 𝜑
44 nfv ⊢ Ⅎ 𝑏 𝑙 Fn ran 𝐺
45 nfra1 ⊢ Ⅎ 𝑏 ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
46 44 45 nfan ⊢ Ⅎ 𝑏 ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
47 43 46 nfan ⊢ Ⅎ 𝑏 ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) )
48 nfv ⊢ Ⅎ 𝑏 ℎ ∈ ran 𝑙
49 47 48 nfan ⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 )
50 simp3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → ( 𝑙 ‘ 𝑏 ) = ℎ )
51 simp1ll ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → 𝜑 )
52 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
53 52 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
54 simp2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → 𝑏 ∈ ran 𝐺 )
55 simp3 ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → 𝑏 ∈ ran 𝐺 )
56 3simpc ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) )
57 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → 𝑏 ∈ ran 𝐺 )
58 rabexg ⊢ ( 𝐴 ∈ V → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
59 13 58 syl ⊢ ( 𝜑 → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
60 59 a1d ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑅 → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V ) )
61 3 60 ralrimi ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
62 6 fnmpt ⊢ ( ∀ 𝑤 ∈ 𝑅 { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V → 𝐺 Fn 𝑅 )
63 61 62 syl ⊢ ( 𝜑 → 𝐺 Fn 𝑅 )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → 𝐺 Fn 𝑅 )
65 fvelrnb ⊢ ( 𝐺 Fn 𝑅 → ( 𝑏 ∈ ran 𝐺 ↔ ∃ 𝑢 ∈ 𝑅 ( 𝐺 ‘ 𝑢 ) = 𝑏 ) )
66 nfmpt1 ⊢ Ⅎ 𝑤 ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
67 6 66 nfcxfr ⊢ Ⅎ 𝑤 𝐺
68 nfcv ⊢ Ⅎ 𝑤 𝑢
69 67 68 nffv ⊢ Ⅎ 𝑤 ( 𝐺 ‘ 𝑢 )
70 nfcv ⊢ Ⅎ 𝑤 𝑏
71 69 70 nfeq ⊢ Ⅎ 𝑤 ( 𝐺 ‘ 𝑢 ) = 𝑏
72 nfv ⊢ Ⅎ 𝑢 ( 𝐺 ‘ 𝑤 ) = 𝑏
73 fveq2 ⊢ ( 𝑢 = 𝑤 → ( 𝐺 ‘ 𝑢 ) = ( 𝐺 ‘ 𝑤 ) )
74 73 eqeq1d ⊢ ( 𝑢 = 𝑤 → ( ( 𝐺 ‘ 𝑢 ) = 𝑏 ↔ ( 𝐺 ‘ 𝑤 ) = 𝑏 ) )
75 71 72 74 cbvrexw ⊢ ( ∃ 𝑢 ∈ 𝑅 ( 𝐺 ‘ 𝑢 ) = 𝑏 ↔ ∃ 𝑤 ∈ 𝑅 ( 𝐺 ‘ 𝑤 ) = 𝑏 )
76 65 75 bitrdi ⊢ ( 𝐺 Fn 𝑅 → ( 𝑏 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑅 ( 𝐺 ‘ 𝑤 ) = 𝑏 ) )
77 64 76 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑏 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑅 ( 𝐺 ‘ 𝑤 ) = 𝑏 ) )
78 57 77 mpbid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → ∃ 𝑤 ∈ 𝑅 ( 𝐺 ‘ 𝑤 ) = 𝑏 )
79 67 nfrn ⊢ Ⅎ 𝑤 ran 𝐺
80 79 nfcri ⊢ Ⅎ 𝑤 𝑏 ∈ ran 𝐺
81 3 80 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 )
82 nfv ⊢ Ⅎ 𝑤 𝑏 ≠ ∅
83 simp3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑤 ) = 𝑏 ) → ( 𝐺 ‘ 𝑤 ) = 𝑏 )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → 𝑤 ∈ 𝑅 )
85 13 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → 𝐴 ∈ V )
86 85 58 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
87 6 fvmpt2 ⊢ ( ( 𝑤 ∈ 𝑅 ∧ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V ) → ( 𝐺 ‘ 𝑤 ) = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
88 84 86 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( 𝐺 ‘ 𝑤 ) = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
89 7 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → 𝑤 ∈ 𝑉 )
90 5 rabeq2i ⊢ ( 𝑤 ∈ 𝑉 ↔ ( 𝑤 ∈ 𝐽 ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) )
91 89 90 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( 𝑤 ∈ 𝐽 ∧ ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ) )
92 91 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) )
93 8 nnrpd ⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
94 10 93 rpdivcld ⊢ ( 𝜑 → ( 𝐸 / 𝑀 ) ∈ ℝ+ )
95 94 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( 𝐸 / 𝑀 ) ∈ ℝ+ )
96 breq2 ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ( ℎ ‘ 𝑡 ) < 𝑒 ↔ ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
97 96 ralbidv ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ↔ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
98 oveq2 ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( 1 − 𝑒 ) = ( 1 − ( 𝐸 / 𝑀 ) ) )
99 98 breq1d ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) )
100 99 ralbidv ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) )
101 97 100 3anbi23d ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) )
102 101 rexbidv ⊢ ( 𝑒 = ( 𝐸 / 𝑀 ) → ( ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ↔ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) )
103 102 rspccva ⊢ ( ( ∀ 𝑒 ∈ ℝ+ ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < 𝑒 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − 𝑒 ) < ( ℎ ‘ 𝑡 ) ) ∧ ( 𝐸 / 𝑀 ) ∈ ℝ+ ) → ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) )
104 92 95 103 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) )
105 nfv ⊢ Ⅎ ℎ 𝑤 ∈ 𝑅
106 1 105 nfan ⊢ Ⅎ ℎ ( 𝜑 ∧ 𝑤 ∈ 𝑅 )
107 nfcv ⊢ Ⅎ ℎ ∅
108 31 107 nfne ⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅
109 3simpc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) ∧ ℎ ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) → ( ℎ ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) )
110 rabid ⊢ ( ℎ ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ↔ ( ℎ ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) )
111 109 110 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) ∧ ℎ ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) → ℎ ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
112 ne0i ⊢ ( ℎ ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅ )
113 111 112 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) ∧ ℎ ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅ )
114 113 3exp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( ℎ ∈ 𝐴 → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅ ) ) )
115 106 108 114 rexlimd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( ∃ ℎ ∈ 𝐴 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅ ) )
116 104 115 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ≠ ∅ )
117 88 116 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ) → ( 𝐺 ‘ 𝑤 ) ≠ ∅ )
118 117 3adant3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑤 ) = 𝑏 ) → ( 𝐺 ‘ 𝑤 ) ≠ ∅ )
119 83 118 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑤 ) = 𝑏 ) → 𝑏 ≠ ∅ )
120 119 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑅 ∧ ( 𝐺 ‘ 𝑤 ) = 𝑏 ) → 𝑏 ≠ ∅ )
121 120 3exp ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑤 ∈ 𝑅 → ( ( 𝐺 ‘ 𝑤 ) = 𝑏 → 𝑏 ≠ ∅ ) ) )
122 81 82 121 rexlimd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → ( ∃ 𝑤 ∈ 𝑅 ( 𝐺 ‘ 𝑤 ) = 𝑏 → 𝑏 ≠ ∅ ) )
123 78 122 mpd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ran 𝐺 ) → 𝑏 ≠ ∅ )
124 123 3adant2 ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → 𝑏 ≠ ∅ )
125 rspa ⊢ ( ( ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
126 56 124 125 sylc ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
127 55 126 jca ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
128 vex ⊢ 𝑏 ∈ V
129 6 elrnmpt ⊢ ( 𝑏 ∈ V → ( 𝑏 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑅 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) )
130 128 129 ax-mp ⊢ ( 𝑏 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑅 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
131 55 130 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ∃ 𝑤 ∈ 𝑅 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
132 nfv ⊢ Ⅎ 𝑤 ( 𝑙 ‘ 𝑏 ) ∈ 𝑏
133 80 132 nfan ⊢ Ⅎ 𝑤 ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
134 nfv ⊢ Ⅎ 𝑤 ( 𝑙 ‘ 𝑏 ) ∈ 𝑌
135 simp1r ⊢ ( ( ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
136 simp3 ⊢ ( ( ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
137 simpl ⊢ ( ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
138 simpr ⊢ ( ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
139 137 138 eleqtrd ⊢ ( ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
140 elrabi ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( 𝑙 ‘ 𝑏 ) ∈ 𝐴 )
141 fveq1 ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ℎ ‘ 𝑡 ) = ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) )
142 141 breq2d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) )
143 141 breq1d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) )
144 142 143 anbi12d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ) )
145 144 ralbidv ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ) )
146 141 breq1d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
147 146 ralbidv ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ∀ 𝑡 ∈ 𝑤 ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
148 141 breq2d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) )
149 148 ralbidv ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) )
150 145 147 149 3anbi123d ⊢ ( ℎ = ( 𝑙 ‘ 𝑏 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) ) )
151 150 elrab ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ↔ ( ( 𝑙 ‘ 𝑏 ) ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) ) )
152 151 simprbi ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ) )
153 152 simp1d ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) )
154 145 elrab ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } ↔ ( ( 𝑙 ‘ 𝑏 ) ∈ 𝐴 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ∧ ( ( 𝑙 ‘ 𝑏 ) ‘ 𝑡 ) ≤ 1 ) ) )
155 140 153 154 sylanbrc ⊢ ( ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
156 139 155 syl ⊢ ( ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) } )
157 156 4 eleqtrrdi ⊢ ( ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 )
158 135 136 157 syl2anc ⊢ ( ( ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑤 ∈ 𝑅 ∧ 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 )
159 158 3exp ⊢ ( ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) → ( 𝑤 ∈ 𝑅 → ( 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 ) ) )
160 133 134 159 rexlimd ⊢ ( ( 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) → ( ∃ 𝑤 ∈ 𝑅 𝑏 = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 ) )
161 127 131 160 sylc ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 )
162 51 53 54 161 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑌 )
163 50 162 eqeltrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) ∧ 𝑏 ∈ ran 𝐺 ∧ ( 𝑙 ‘ 𝑏 ) = ℎ ) → ℎ ∈ 𝑌 )
164 163 3exp ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ( 𝑏 ∈ ran 𝐺 → ( ( 𝑙 ‘ 𝑏 ) = ℎ → ℎ ∈ 𝑌 ) ) )
165 49 164 reximdai ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ( ∃ 𝑏 ∈ ran 𝐺 ( 𝑙 ‘ 𝑏 ) = ℎ → ∃ 𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 ) )
166 42 165 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ∃ 𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 )
167 nfv ⊢ Ⅎ 𝑏 ℎ ∈ 𝑌
168 idd ⊢ ( 𝑏 ∈ ran 𝐺 → ( ℎ ∈ 𝑌 → ℎ ∈ 𝑌 ) )
169 168 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ( 𝑏 ∈ ran 𝐺 → ( ℎ ∈ 𝑌 → ℎ ∈ 𝑌 ) ) )
170 49 167 169 rexlimd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ( ∃ 𝑏 ∈ ran 𝐺 ℎ ∈ 𝑌 → ℎ ∈ 𝑌 ) )
171 166 170 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ ℎ ∈ ran 𝑙 ) → ℎ ∈ 𝑌 )
172 171 ex ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( ℎ ∈ ran 𝑙 → ℎ ∈ 𝑌 ) )
173 39 172 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ∀ ℎ ∈ ran 𝑙 ℎ ∈ 𝑌 )
174 dfss3 ⊢ ( ran 𝑙 ⊆ 𝑌 ↔ ∀ 𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 )
175 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) }
176 4 175 nfcxfr ⊢ Ⅎ ℎ 𝑌
177 176 nfcri ⊢ Ⅎ ℎ 𝑧 ∈ 𝑌
178 nfv ⊢ Ⅎ 𝑧 ℎ ∈ 𝑌
179 eleq1 ⊢ ( 𝑧 = ℎ → ( 𝑧 ∈ 𝑌 ↔ ℎ ∈ 𝑌 ) )
180 177 178 179 cbvralw ⊢ ( ∀ 𝑧 ∈ ran 𝑙 𝑧 ∈ 𝑌 ↔ ∀ ℎ ∈ ran 𝑙 ℎ ∈ 𝑌 )
181 174 180 bitri ⊢ ( ran 𝑙 ⊆ 𝑌 ↔ ∀ ℎ ∈ ran 𝑙 ℎ ∈ 𝑌 )
182 173 181 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ran 𝑙 ⊆ 𝑌 )
183 df-f ⊢ ( 𝑙 : ran 𝐺 ⟶ 𝑌 ↔ ( 𝑙 Fn ran 𝐺 ∧ ran 𝑙 ⊆ 𝑌 ) )
184 28 182 183 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → 𝑙 : ran 𝐺 ⟶ 𝑌 )
185 dffn3 ⊢ ( 𝐺 Fn 𝑅 ↔ 𝐺 : 𝑅 ⟶ ran 𝐺 )
186 63 185 sylib ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ran 𝐺 )
187 186 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → 𝐺 : 𝑅 ⟶ ran 𝐺 )
188 f1of ⊢ ( 𝑣 : ( 1 ... 𝑀 ) –1-1-onto→ 𝑅 → 𝑣 : ( 1 ... 𝑀 ) ⟶ 𝑅 )
189 9 188 syl ⊢ ( 𝜑 → 𝑣 : ( 1 ... 𝑀 ) ⟶ 𝑅 )
190 189 adantr ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → 𝑣 : ( 1 ... 𝑀 ) ⟶ 𝑅 )
191 fco ⊢ ( ( 𝐺 : 𝑅 ⟶ ran 𝐺 ∧ 𝑣 : ( 1 ... 𝑀 ) ⟶ 𝑅 ) → ( 𝐺 ∘ 𝑣 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐺 )
192 187 190 191 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( 𝐺 ∘ 𝑣 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐺 )
193 fco ⊢ ( ( 𝑙 : ran 𝐺 ⟶ 𝑌 ∧ ( 𝐺 ∘ 𝑣 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐺 ) → ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 )
194 184 192 193 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 )
195 fvco3 ⊢ ( ( ( 𝐺 ∘ 𝑣 ) : ( 1 ... 𝑀 ) ⟶ ran 𝐺 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) = ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) )
196 192 195 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) = ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) )
197 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝜑 )
198 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
199 192 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 )
200 simp3 ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 )
201 nfv ⊢ Ⅎ 𝑏 ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺
202 43 45 201 nf3an ⊢ Ⅎ 𝑏 ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 )
203 nfv ⊢ Ⅎ 𝑏 ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 )
204 202 203 nfim ⊢ Ⅎ 𝑏 ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) → ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) )
205 eleq1 ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ( 𝑏 ∈ ran 𝐺 ↔ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) )
206 205 3anbi3d ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) ) )
207 fveq2 ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ( 𝑙 ‘ 𝑏 ) = ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) )
208 id ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) )
209 207 208 eleq12d ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ( ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ↔ ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) )
210 206 209 imbi12d ⊢ ( 𝑏 = ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ( ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ 𝑏 ∈ ran 𝐺 ) → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ↔ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) → ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ) )
211 204 210 126 vtoclg1f ⊢ ( ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 → ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) → ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) )
212 200 211 mpcom ⊢ ( ( 𝜑 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ∧ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ∈ ran 𝐺 ) → ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) )
213 197 198 199 212 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑙 ‘ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) )
214 196 213 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) )
215 fvco3 ⊢ ( ( 𝑣 : ( 1 ... 𝑀 ) ⟶ 𝑅 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝑣 ‘ 𝑖 ) ) )
216 189 215 sylan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) = ( 𝐺 ‘ ( 𝑣 ‘ 𝑖 ) ) )
217 raleq ⊢ ( 𝑤 = ( 𝑣 ‘ 𝑖 ) → ( ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
218 217 3anbi2d ⊢ ( 𝑤 = ( 𝑣 ‘ 𝑖 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ) )
219 218 rabbidv ⊢ ( 𝑤 = ( 𝑣 ‘ 𝑖 ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
220 189 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑣 ‘ 𝑖 ) ∈ 𝑅 )
221 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐴 ∈ V )
222 rabexg ⊢ ( 𝐴 ∈ V → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
223 221 222 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ∈ V )
224 6 219 220 223 fvmptd3 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐺 ‘ ( 𝑣 ‘ 𝑖 ) ) = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
225 216 224 eqtrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
226 225 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) = { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
227 226 eleq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) ↔ ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ) )
228 nfcv ⊢ Ⅎ ℎ 𝑣
229 33 228 nfco ⊢ Ⅎ ℎ ( 𝐺 ∘ 𝑣 )
230 29 229 nfco ⊢ Ⅎ ℎ ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) )
231 nfcv ⊢ Ⅎ ℎ 𝑖
232 230 231 nffv ⊢ Ⅎ ℎ ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 )
233 nfcv ⊢ Ⅎ ℎ 𝐴
234 nfcv ⊢ Ⅎ ℎ 𝑇
235 nfcv ⊢ Ⅎ ℎ 0
236 nfcv ⊢ Ⅎ ℎ ≤
237 nfcv ⊢ Ⅎ ℎ 𝑡
238 232 237 nffv ⊢ Ⅎ ℎ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 )
239 235 236 238 nfbr ⊢ Ⅎ ℎ 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 )
240 nfcv ⊢ Ⅎ ℎ 1
241 238 236 240 nfbr ⊢ Ⅎ ℎ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1
242 239 241 nfan ⊢ Ⅎ ℎ ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
243 234 242 nfralw ⊢ Ⅎ ℎ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 )
244 nfcv ⊢ Ⅎ ℎ ( 𝑣 ‘ 𝑖 )
245 nfcv ⊢ Ⅎ ℎ <
246 nfcv ⊢ Ⅎ ℎ ( 𝐸 / 𝑀 )
247 238 245 246 nfbr ⊢ Ⅎ ℎ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 )
248 244 247 nfralw ⊢ Ⅎ ℎ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 )
249 nfcv ⊢ Ⅎ ℎ ( 𝑇 ∖ 𝑈 )
250 nfcv ⊢ Ⅎ ℎ ( 1 − ( 𝐸 / 𝑀 ) )
251 250 245 238 nfbr ⊢ Ⅎ ℎ ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 )
252 249 251 nfralw ⊢ Ⅎ ℎ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 )
253 243 248 252 nf3an ⊢ Ⅎ ℎ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
254 nfcv ⊢ Ⅎ 𝑡 ℎ
255 nfcv ⊢ Ⅎ 𝑡 𝑙
256 nfcv ⊢ Ⅎ 𝑡 𝑅
257 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
258 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 )
259 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 )
260 257 258 259 nf3an ⊢ Ⅎ 𝑡 ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) )
261 nfcv ⊢ Ⅎ 𝑡 𝐴
262 260 261 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) }
263 256 262 nfmpt ⊢ Ⅎ 𝑡 ( 𝑤 ∈ 𝑅 ↦ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ 𝑤 ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } )
264 6 263 nfcxfr ⊢ Ⅎ 𝑡 𝐺
265 nfcv ⊢ Ⅎ 𝑡 𝑣
266 264 265 nfco ⊢ Ⅎ 𝑡 ( 𝐺 ∘ 𝑣 )
267 255 266 nfco ⊢ Ⅎ 𝑡 ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) )
268 nfcv ⊢ Ⅎ 𝑡 𝑖
269 267 268 nffv ⊢ Ⅎ 𝑡 ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 )
270 254 269 nfeq ⊢ Ⅎ 𝑡 ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 )
271 fveq1 ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ℎ ‘ 𝑡 ) = ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
272 271 breq2d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
273 271 breq1d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) )
274 272 273 anbi12d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
275 270 274 ralbid ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ) )
276 271 breq1d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
277 270 276 ralbid ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
278 271 breq2d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
279 270 278 ralbid ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
280 275 277 279 3anbi123d ⊢ ( ℎ = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) → ( ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
281 232 233 253 280 elrabf ⊢ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } ↔ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ 𝐴 ∧ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
282 281 simprbi ⊢ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ∧ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
283 282 simp2d ⊢ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
284 227 283 syl6bi ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
285 214 284 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) )
286 264 nfrn ⊢ Ⅎ 𝑡 ran 𝐺
287 255 286 nffn ⊢ Ⅎ 𝑡 𝑙 Fn ran 𝐺
288 nfv ⊢ Ⅎ 𝑡 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
289 286 288 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 )
290 287 289 nfan ⊢ Ⅎ 𝑡 ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) )
291 2 290 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) )
292 nfv ⊢ Ⅎ 𝑡 𝑖 ∈ ( 1 ... 𝑀 )
293 291 292 nfan ⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) )
294 11 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝐵 ) → 𝐵 ⊆ ( 𝑇 ∖ 𝑈 ) )
295 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ 𝐵 )
296 294 295 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝐵 ) → 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) )
297 282 simp3d ⊢ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝐴 ∣ ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ∧ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ℎ ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ℎ ‘ 𝑡 ) ) } → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
298 227 297 syl6bi ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ∈ ( ( 𝐺 ∘ 𝑣 ) ‘ 𝑖 ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
299 214 298 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
300 299 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
301 296 300 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) ∧ 𝑡 ∈ 𝐵 ) → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
302 301 ex ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝑡 ∈ 𝐵 → ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
303 293 302 ralrimi ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
304 285 303 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
305 304 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
306 194 305 jca ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
307 feq1 ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ↔ ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 ) )
308 nfcv ⊢ Ⅎ 𝑡 𝑥
309 308 267 nfeq ⊢ Ⅎ 𝑡 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) )
310 fveq1 ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( 𝑥 ‘ 𝑖 ) = ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) )
311 310 fveq1d ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) )
312 311 breq1d ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
313 309 312 ralbid ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ↔ ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ) )
314 311 breq2d ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ↔ ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
315 309 314 ralbid ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
316 313 315 anbi12d ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
317 316 ralbidv ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
318 307 317 anbi12d ⊢ ( 𝑥 = ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) → ( ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ↔ ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
319 318 spcegv ⊢ ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ∈ V → ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( ( 𝑙 ∘ ( 𝐺 ∘ 𝑣 ) ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
320 27 306 319 sylc ⊢ ( ( 𝜑 ∧ ( 𝑙 Fn ran 𝐺 ∧ ∀ 𝑏 ∈ ran 𝐺 ( 𝑏 ≠ ∅ → ( 𝑙 ‘ 𝑏 ) ∈ 𝑏 ) ) ) → ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
321 16 320 exlimddv ⊢ ( 𝜑 → ∃ 𝑥 ( 𝑥 : ( 1 ... 𝑀 ) ⟶ 𝑌 ∧ ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ∀ 𝑡 ∈ ( 𝑣 ‘ 𝑖 ) ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) < ( 𝐸 / 𝑀 ) ∧ ∀ 𝑡 ∈ 𝐵 ( 1 − ( 𝐸 / 𝑀 ) ) < ( ( 𝑥 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )