Metamath Proof Explorer

Theorem stoweidlem27

Description: This lemma is used to prove the existence of a function p as in Lemma 1 BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem27.1 ⊢ 𝐺 = ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
stoweidlem27.2 ⊢ ( 𝜑 → 𝑄 ∈ V )
stoweidlem27.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
stoweidlem27.4 ⊢ ( 𝜑 → 𝑌 Fn ran 𝐺 )
stoweidlem27.5 ⊢ ( 𝜑 → ran 𝐺 ∈ V )
stoweidlem27.6 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 )
stoweidlem27.7 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐺 )
stoweidlem27.8 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑋 )
stoweidlem27.9 ⊢ Ⅎ 𝑡 𝜑
stoweidlem27.10 ⊢ Ⅎ 𝑤 𝜑
stoweidlem27.11 ⊢ Ⅎ ℎ 𝑄
Assertion stoweidlem27 ( 𝜑 → ∃ 𝑞 ( 𝑀 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem27.1 ⊢ 𝐺 = ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
2 stoweidlem27.2 ⊢ ( 𝜑 → 𝑄 ∈ V )
3 stoweidlem27.3 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 stoweidlem27.4 ⊢ ( 𝜑 → 𝑌 Fn ran 𝐺 )
5 stoweidlem27.5 ⊢ ( 𝜑 → ran 𝐺 ∈ V )
6 stoweidlem27.6 ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 )
7 stoweidlem27.7 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐺 )
8 stoweidlem27.8 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑋 )
9 stoweidlem27.9 ⊢ Ⅎ 𝑡 𝜑
10 stoweidlem27.10 ⊢ Ⅎ 𝑤 𝜑
11 stoweidlem27.11 ⊢ Ⅎ ℎ 𝑄
12 fnex ⊢ ( ( 𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V ) → 𝑌 ∈ V )
13 4 5 12 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ V )
14 f1ofn ⊢ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐺 → 𝐹 Fn ( 1 ... 𝑀 ) )
15 7 14 syl ⊢ ( 𝜑 → 𝐹 Fn ( 1 ... 𝑀 ) )
16 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
17 fnex ⊢ ( ( 𝐹 Fn ( 1 ... 𝑀 ) ∧ ( 1 ... 𝑀 ) ∈ V ) → 𝐹 ∈ V )
18 15 16 17 sylancl ⊢ ( 𝜑 → 𝐹 ∈ V )
19 coexg ⊢ ( ( 𝑌 ∈ V ∧ 𝐹 ∈ V ) → ( 𝑌 ∘ 𝐹 ) ∈ V )
20 13 18 19 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∘ 𝐹 ) ∈ V )
21 f1of ⊢ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐺 → 𝐹 : ( 1 ... 𝑀 ) ⟶ ran 𝐺 )
22 7 21 syl ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑀 ) ⟶ ran 𝐺 )
23 fnfco ⊢ ( ( 𝑌 Fn ran 𝐺 ∧ 𝐹 : ( 1 ... 𝑀 ) ⟶ ran 𝐺 ) → ( 𝑌 ∘ 𝐹 ) Fn ( 1 ... 𝑀 ) )
24 4 22 23 syl2anc ⊢ ( 𝜑 → ( 𝑌 ∘ 𝐹 ) Fn ( 1 ... 𝑀 ) )
25 rncoss ⊢ ran ( 𝑌 ∘ 𝐹 ) ⊆ ran 𝑌
26 fvelrnb ⊢ ( 𝑌 Fn ran 𝐺 → ( 𝑘 ∈ ran 𝑌 ↔ ∃ 𝑙 ∈ ran 𝐺 ( 𝑌 ‘ 𝑙 ) = 𝑘 ) )
27 4 26 syl ⊢ ( 𝜑 → ( 𝑘 ∈ ran 𝑌 ↔ ∃ 𝑙 ∈ ran 𝐺 ( 𝑌 ‘ 𝑙 ) = 𝑘 ) )
28 27 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → ∃ 𝑙 ∈ ran 𝐺 ( 𝑌 ‘ 𝑙 ) = 𝑘 )
29 nfmpt1 ⊢ Ⅎ 𝑤 ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
30 1 29 nfcxfr ⊢ Ⅎ 𝑤 𝐺
31 30 nfrn ⊢ Ⅎ 𝑤 ran 𝐺
32 31 nfcri ⊢ Ⅎ 𝑤 𝑙 ∈ ran 𝐺
33 10 32 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 )
34 6 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 )
35 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
36 34 35 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( 𝑌 ‘ 𝑙 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
37 nfcv ⊢ Ⅎ ℎ ( 𝑌 ‘ 𝑙 )
38 nfv ⊢ Ⅎ ℎ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) }
39 fveq1 ⊢ ( ℎ = ( 𝑌 ‘ 𝑙 ) → ( ℎ ‘ 𝑡 ) = ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) )
40 39 breq2d ⊢ ( ℎ = ( 𝑌 ‘ 𝑙 ) → ( 0 < ( ℎ ‘ 𝑡 ) ↔ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) ) )
41 40 rabbidv ⊢ ( ℎ = ( 𝑌 ‘ 𝑙 ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) } )
42 41 eqeq2d ⊢ ( ℎ = ( 𝑌 ‘ 𝑙 ) → ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) } ) )
43 37 11 38 42 elrabf ⊢ ( ( 𝑌 ‘ 𝑙 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ( ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) } ) )
44 36 43 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( 𝑌 ‘ 𝑙 ) ‘ 𝑡 ) } ) )
45 44 simpld ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → 𝑙 ∈ ran 𝐺 )
47 1 elrnmpt ⊢ ( 𝑙 ∈ ran 𝐺 → ( 𝑙 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑋 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) )
48 46 47 syl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑙 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑋 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) )
49 46 48 mpbid ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ∃ 𝑤 ∈ 𝑋 𝑙 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
50 33 45 49 r19.29af ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 )
51 50 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 )
52 eleq1 ⊢ ( ( 𝑌 ‘ 𝑙 ) = 𝑘 → ( ( 𝑌 ‘ 𝑙 ) ∈ 𝑄 ↔ 𝑘 ∈ 𝑄 ) )
53 51 52 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) ∧ 𝑙 ∈ ran 𝐺 ) → ( ( 𝑌 ‘ 𝑙 ) = 𝑘 → 𝑘 ∈ 𝑄 ) )
54 53 reximdva ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → ( ∃ 𝑙 ∈ ran 𝐺 ( 𝑌 ‘ 𝑙 ) = 𝑘 → ∃ 𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 ) )
55 28 54 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → ∃ 𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 )
56 idd ⊢ ( 𝑙 ∈ ran 𝐺 → ( 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄 ) )
57 56 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → ( 𝑙 ∈ ran 𝐺 → ( 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄 ) ) )
58 57 rexlimdv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → ( ∃ 𝑙 ∈ ran 𝐺 𝑘 ∈ 𝑄 → 𝑘 ∈ 𝑄 ) )
59 55 58 mpd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝑌 ) → 𝑘 ∈ 𝑄 )
60 59 ex ⊢ ( 𝜑 → ( 𝑘 ∈ ran 𝑌 → 𝑘 ∈ 𝑄 ) )
61 60 ssrdv ⊢ ( 𝜑 → ran 𝑌 ⊆ 𝑄 )
62 25 61 sstrid ⊢ ( 𝜑 → ran ( 𝑌 ∘ 𝐹 ) ⊆ 𝑄 )
63 df-f ⊢ ( ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ↔ ( ( 𝑌 ∘ 𝐹 ) Fn ( 1 ... 𝑀 ) ∧ ran ( 𝑌 ∘ 𝐹 ) ⊆ 𝑄 ) )
64 24 62 63 sylanbrc ⊢ ( 𝜑 → ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 )
65 nfv ⊢ Ⅎ 𝑤 𝑡 ∈ ( 𝑇 ∖ 𝑈 )
66 10 65 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) )
67 nfv ⊢ Ⅎ 𝑤 ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 )
68 8 sselda ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑡 ∈ ∪ 𝑋 )
69 eluni ⊢ ( 𝑡 ∈ ∪ 𝑋 ↔ ∃ 𝑤 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) )
70 68 69 sylib ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑤 ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) )
71 1 funmpt2 ⊢ Fun 𝐺
72 1 dmeqi ⊢ dom 𝐺 = dom ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
73 11 rabexgf ⊢ ( 𝑄 ∈ V → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
74 2 73 syl ⊢ ( 𝜑 → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
75 74 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
76 75 ex ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑋 → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V ) )
77 10 76 ralrimi ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑋 { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
78 dmmptg ⊢ ( ∀ 𝑤 ∈ 𝑋 { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V → dom ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) = 𝑋 )
79 77 78 syl ⊢ ( 𝜑 → dom ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) = 𝑋 )
80 72 79 syl5eq ⊢ ( 𝜑 → dom 𝐺 = 𝑋 )
81 80 eleq2d ⊢ ( 𝜑 → ( 𝑤 ∈ dom 𝐺 ↔ 𝑤 ∈ 𝑋 ) )
82 81 biimpar ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ dom 𝐺 )
83 fvelrn ⊢ ( ( Fun 𝐺 ∧ 𝑤 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 )
84 71 82 83 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 )
85 84 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 )
86 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → 𝐹 : ( 1 ... 𝑀 ) ⟶ ran 𝐺 )
87 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → 𝑖 ∈ ( 1 ... 𝑀 ) )
88 fvco3 ⊢ ( ( 𝐹 : ( 1 ... 𝑀 ) ⟶ ran 𝐺 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) = ( 𝑌 ‘ ( 𝐹 ‘ 𝑖 ) ) )
89 86 87 88 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) = ( 𝑌 ‘ ( 𝐹 ‘ 𝑖 ) ) )
90 fveq2 ⊢ ( ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) → ( 𝑌 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) )
91 90 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → ( 𝑌 ‘ ( 𝐹 ‘ 𝑖 ) ) = ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) )
92 89 91 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) = ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) )
93 eleq1 ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( 𝑙 ∈ ran 𝐺 ↔ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) )
94 93 anbi2d ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) ↔ ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ) )
95 eleq2 ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑌 ‘ 𝑙 ) ∈ ( 𝐺 ‘ 𝑤 ) ) )
96 fveq2 ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( 𝑌 ‘ 𝑙 ) = ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) )
97 96 eleq1d ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑌 ‘ 𝑙 ) ∈ ( 𝐺 ‘ 𝑤 ) ↔ ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) ) )
98 95 97 bitrd ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) ) )
99 94 98 imbi12d ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑤 ) → ( ( ( 𝜑 ∧ 𝑙 ∈ ran 𝐺 ) → ( 𝑌 ‘ 𝑙 ) ∈ 𝑙 ) ↔ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) ) ) )
100 99 6 vtoclg ⊢ ( ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 → ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) ) )
101 100 anabsi7 ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) )
102 101 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → ( 𝑌 ‘ ( 𝐺 ‘ 𝑤 ) ) ∈ ( 𝐺 ‘ 𝑤 ) )
103 92 102 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) ∧ ( 𝑖 ∈ ( 1 ... 𝑀 ) ∧ ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) )
104 f1ofo ⊢ ( 𝐹 : ( 1 ... 𝑀 ) –1-1-onto→ ran 𝐺 → 𝐹 : ( 1 ... 𝑀 ) –onto→ ran 𝐺 )
105 forn ⊢ ( 𝐹 : ( 1 ... 𝑀 ) –onto→ ran 𝐺 → ran 𝐹 = ran 𝐺 )
106 7 104 105 3syl ⊢ ( 𝜑 → ran 𝐹 = ran 𝐺 )
107 106 eleq2d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐹 ↔ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) )
108 107 biimpar ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐹 )
109 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → 𝐹 Fn ( 1 ... 𝑀 ) )
110 fvelrnb ⊢ ( 𝐹 Fn ( 1 ... 𝑀 ) → ( ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐹 ↔ ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) )
111 109 110 syl ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ( ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐹 ↔ ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) ) )
112 108 111 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝐹 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑤 ) )
113 103 112 reximddv ⊢ ( ( 𝜑 ∧ ( 𝐺 ‘ 𝑤 ) ∈ ran 𝐺 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) )
114 85 113 syldan ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) )
115 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → 𝑡 ∈ 𝑤 )
116 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝑋 )
117 1 fvmpt2 ⊢ ( ( 𝑤 ∈ 𝑋 ∧ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V ) → ( 𝐺 ‘ 𝑤 ) = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
118 116 75 117 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑤 ) = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
119 118 eleq2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ↔ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) )
120 119 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
121 120 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
122 nfcv ⊢ Ⅎ ℎ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 )
123 nfv ⊢ Ⅎ ℎ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) }
124 fveq1 ⊢ ( ℎ = ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) → ( ℎ ‘ 𝑡 ) = ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
125 124 breq2d ⊢ ( ℎ = ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) → ( 0 < ( ℎ ‘ 𝑡 ) ↔ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
126 125 rabbidv ⊢ ( ℎ = ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } )
127 126 eqeq2d ⊢ ( ℎ = ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) → ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } ) )
128 122 11 123 127 elrabf ⊢ ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } ) )
129 121 128 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } ) )
130 129 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } )
131 115 130 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } )
132 rabid ⊢ ( 𝑡 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) } ↔ ( 𝑡 ∈ 𝑇 ∧ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
133 131 132 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → ( 𝑡 ∈ 𝑇 ∧ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
134 133 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) ∧ ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) ) → 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
135 134 ex ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) → 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
136 135 reximdv ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) → ( ∃ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ∈ ( 𝐺 ‘ 𝑤 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
137 114 136 mpd ⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
138 137 ex ⊢ ( 𝜑 → ( ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ( ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑋 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
140 66 67 70 139 exlimimdd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
141 140 ex ⊢ ( 𝜑 → ( 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) → ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
142 9 141 ralrimi ⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
143 3 64 142 jca32 ⊢ ( 𝜑 → ( 𝑀 ∈ ℕ ∧ ( ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
144 feq1 ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ↔ ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ) )
145 fveq1 ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( 𝑞 ‘ 𝑖 ) = ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) )
146 145 fveq1d ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) = ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) )
147 146 breq2d ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ↔ 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
148 147 rexbidv ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ↔ ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
149 148 ralbidv ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ↔ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) )
150 144 149 anbi12d ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ↔ ( ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
151 150 anbi2d ⊢ ( 𝑞 = ( 𝑌 ∘ 𝐹 ) → ( ( 𝑀 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ↔ ( 𝑀 ∈ ℕ ∧ ( ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
152 151 spcegv ⊢ ( ( 𝑌 ∘ 𝐹 ) ∈ V → ( ( 𝑀 ∈ ℕ ∧ ( ( 𝑌 ∘ 𝐹 ) : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( ( 𝑌 ∘ 𝐹 ) ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑞 ( 𝑀 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
153 20 143 152 sylc ⊢ ( 𝜑 → ∃ 𝑞 ( 𝑀 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑀 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑀 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )