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 ⊢ Ⅎ h φ
stoweidlem31.2 ⊢ Ⅎ t φ
stoweidlem31.3 ⊢ Ⅎ w φ
stoweidlem31.4 ⊢ Y = h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1
stoweidlem31.5 ⊢ V = w ∈ J | ∀ e ∈ ℝ + ∃ h ∈ A ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < e ∧ ∀ t ∈ T ∖ U 1 − e < h ⁡ t
stoweidlem31.6 ⊢ G = w ∈ R ⟼ h ∈ A | ∀ t ∈ T 0 ≤ h ⁡ t ∧ h ⁡ t ≤ 1 ∧ ∀ t ∈ w h ⁡ t < E M ∧ ∀ t ∈ T ∖ U 1 − E M < h ⁡ t
stoweidlem31.7 ⊢ φ → R ⊆ V
stoweidlem31.8 ⊢ φ → M ∈ ℕ
stoweidlem31.9 ⊢ φ → v : 1 … M ⟶ 1-1 onto R
stoweidlem31.10 ⊢ φ → E ∈ ℝ +
stoweidlem31.11 ⊢ φ → B ⊆ T ∖ U
stoweidlem31.12 ⊢ φ → V ∈ V
stoweidlem31.13 ⊢ φ → A ∈ V
stoweidlem31.14 ⊢ φ → ran ⁡ G ∈ Fin
Assertion stoweidlem31 ⊢ φ → ∃ x x : 1 … M ⟶ Y ∧ ∀ i ∈ 1 … M ∀ t ∈ v ⁡ i x ⁡ i ⁡ t < E M ∧ ∀ t ∈ B 1 − E M < x ⁡ i ⁡ t

Proof

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