Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem27 Structured version   Visualization version   GIF version

Theorem stoweidlem27 38920
 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 (𝑞‘𝑖) is used to represent p(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
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
Ref Expression
stoweidlem27 (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))))
Distinct variable groups:   ,𝑖,𝑡,𝑤,𝐹   ,𝑙,𝑌,𝑡,𝑤   𝑇,,𝑤   𝑖,𝑞,𝑡,𝐹   𝑖,𝐺   𝑖,𝑀,𝑞   𝑖,𝑋,𝑤   𝑖,𝑌,𝑞   𝜑,𝑖   𝑄,𝑙   𝜑,𝑙   𝐺,𝑙   𝑄,𝑞   𝑇,𝑞   𝑈,𝑞   𝑤,𝑀   𝑤,𝑄   𝑤,𝑈
Allowed substitution hints:   𝜑(𝑤,𝑡,,𝑞)   𝑄(𝑡,,𝑖)   𝑇(𝑡,𝑖,𝑙)   𝑈(𝑡,,𝑖,𝑙)   𝐹(𝑙)   𝐺(𝑤,𝑡,,𝑞)   𝑀(𝑡,,𝑙)   𝑋(𝑡,,𝑞,𝑙)

Proof of Theorem stoweidlem27
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 stoweidlem27.4 . . . 4 (𝜑𝑌 Fn ran 𝐺)
2 stoweidlem27.5 . . . 4 (𝜑 → ran 𝐺 ∈ V)
3 fnex 6386 . . . 4 ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
41, 2, 3syl2anc 691 . . 3 (𝜑𝑌 ∈ V)
5 stoweidlem27.7 . . . . 5 (𝜑𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6 f1ofn 6051 . . . . 5 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹 Fn (1...𝑀))
75, 6syl 17 . . . 4 (𝜑𝐹 Fn (1...𝑀))
8 ovex 6577 . . . 4 (1...𝑀) ∈ V
9 fnex 6386 . . . 4 ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 693 . . 3 (𝜑𝐹 ∈ V)
11 coexg 7010 . . 3 ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌𝐹) ∈ V)
124, 10, 11syl2anc 691 . 2 (𝜑 → (𝑌𝐹) ∈ V)
13 stoweidlem27.3 . . 3 (𝜑𝑀 ∈ ℕ)
14 f1of 6050 . . . . . 6 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺)
155, 14syl 17 . . . . 5 (𝜑𝐹:(1...𝑀)⟶ran 𝐺)
16 fnfco 5982 . . . . 5 ((𝑌 Fn ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌𝐹) Fn (1...𝑀))
171, 15, 16syl2anc 691 . . . 4 (𝜑 → (𝑌𝐹) Fn (1...𝑀))
18 rncoss 5307 . . . . 5 ran (𝑌𝐹) ⊆ ran 𝑌
19 fvelrnb 6153 . . . . . . . . . . 11 (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
201, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
2120biimpa 500 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘)
22 stoweidlem27.10 . . . . . . . . . . . . . 14 𝑤𝜑
23 stoweidlem27.1 . . . . . . . . . . . . . . . . 17 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
24 nfmpt1 4675 . . . . . . . . . . . . . . . . 17 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2523, 24nfcxfr 2749 . . . . . . . . . . . . . . . 16 𝑤𝐺
2625nfrn 5289 . . . . . . . . . . . . . . 15 𝑤ran 𝐺
2726nfcri 2745 . . . . . . . . . . . . . 14 𝑤 𝑙 ∈ ran 𝐺
2822, 27nfan 1816 . . . . . . . . . . . . 13 𝑤(𝜑𝑙 ∈ ran 𝐺)
29 stoweidlem27.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙)
3029ad2antrr 758 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑙)
31 simpr 476 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
3230, 31eleqtrd 2690 . . . . . . . . . . . . . . 15 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 nfcv 2751 . . . . . . . . . . . . . . . 16 (𝑌𝑙)
34 stoweidlem27.11 . . . . . . . . . . . . . . . 16 𝑄
35 nfv 1830 . . . . . . . . . . . . . . . 16 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}
36 fveq1 6102 . . . . . . . . . . . . . . . . . . 19 ( = (𝑌𝑙) → (𝑡) = ((𝑌𝑙)‘𝑡))
3736breq2d 4595 . . . . . . . . . . . . . . . . . 18 ( = (𝑌𝑙) → (0 < (𝑡) ↔ 0 < ((𝑌𝑙)‘𝑡)))
3837rabbidv 3164 . . . . . . . . . . . . . . . . 17 ( = (𝑌𝑙) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)})
3938eqeq2d 2620 . . . . . . . . . . . . . . . 16 ( = (𝑌𝑙) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4033, 34, 35, 39elrabf 3329 . . . . . . . . . . . . . . 15 ((𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4132, 40sylib 207 . . . . . . . . . . . . . 14 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4241simpld 474 . . . . . . . . . . . . 13 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑄)
43 simpr 476 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
4423elrnmpt 5293 . . . . . . . . . . . . . . 15 (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4543, 44syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4643, 45mpbid 221 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ran 𝐺) → ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4728, 42, 46r19.29af 3058 . . . . . . . . . . . 12 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
4847adantlr 747 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
49 eleq1 2676 . . . . . . . . . . 11 ((𝑌𝑙) = 𝑘 → ((𝑌𝑙) ∈ 𝑄𝑘𝑄))
5048, 49syl5ibcom 234 . . . . . . . . . 10 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌𝑙) = 𝑘𝑘𝑄))
5150reximdva 3000 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘𝑄))
5221, 51mpd 15 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘𝑄)
53 idd 24 . . . . . . . . . 10 (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄))
5453a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄)))
5554rexlimdv 3012 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘𝑄𝑘𝑄))
5652, 55mpd 15 . . . . . . 7 ((𝜑𝑘 ∈ ran 𝑌) → 𝑘𝑄)
5756ex 449 . . . . . 6 (𝜑 → (𝑘 ∈ ran 𝑌𝑘𝑄))
5857ssrdv 3574 . . . . 5 (𝜑 → ran 𝑌𝑄)
5918, 58syl5ss 3579 . . . 4 (𝜑 → ran (𝑌𝐹) ⊆ 𝑄)
60 df-f 5808 . . . 4 ((𝑌𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌𝐹) Fn (1...𝑀) ∧ ran (𝑌𝐹) ⊆ 𝑄))
6117, 59, 60sylanbrc 695 . . 3 (𝜑 → (𝑌𝐹):(1...𝑀)⟶𝑄)
62 stoweidlem27.9 . . . 4 𝑡𝜑
63 stoweidlem27.8 . . . . . . . . 9 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
6463sselda 3568 . . . . . . . 8 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝑡 𝑋)
65 eluni 4375 . . . . . . . 8 (𝑡 𝑋 ↔ ∃𝑤(𝑡𝑤𝑤𝑋))
6664, 65sylib 207 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤(𝑡𝑤𝑤𝑋))
67 nfv 1830 . . . . . . . . 9 𝑤 𝑡 ∈ (𝑇𝑈)
6822, 67nfan 1816 . . . . . . . 8 𝑤(𝜑𝑡 ∈ (𝑇𝑈))
6923funmpt2 5841 . . . . . . . . . . . . . 14 Fun 𝐺
7023dmeqi 5247 . . . . . . . . . . . . . . . . 17 dom 𝐺 = dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
71 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑄 ∈ V)
7234rabexgf 38206 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7473adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7574ex 449 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤𝑋 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V))
7622, 75ralrimi 2940 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
77 dmmptg 5549 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7876, 77syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7970, 78syl5eq 2656 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐺 = 𝑋)
8079eleq2d 2673 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ dom 𝐺𝑤𝑋))
8180biimpar 501 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑋) → 𝑤 ∈ dom 𝐺)
82 fvelrn 6260 . . . . . . . . . . . . . 14 ((Fun 𝐺𝑤 ∈ dom 𝐺) → (𝐺𝑤) ∈ ran 𝐺)
8369, 81, 82sylancr 694 . . . . . . . . . . . . 13 ((𝜑𝑤𝑋) → (𝐺𝑤) ∈ ran 𝐺)
8483adantrl 748 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (𝐺𝑤) ∈ ran 𝐺)
8515ad2antrr 758 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
86 simprl 790 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝑖 ∈ (1...𝑀))
87 fvco3 6185 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑀)⟶ran 𝐺𝑖 ∈ (1...𝑀)) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
8885, 86, 87syl2anc 691 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
89 fveq2 6103 . . . . . . . . . . . . . . . 16 ((𝐹𝑖) = (𝐺𝑤) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9089ad2antll 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9188, 90eqtrd 2644 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐺𝑤)))
92 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺𝑤) ∈ ran 𝐺))
9392anbi2d 736 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → ((𝜑𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺)))
94 eleq2 2677 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌𝑙) ∈ (𝐺𝑤)))
95 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = (𝐺𝑤) → (𝑌𝑙) = (𝑌‘(𝐺𝑤)))
9695eleq1d 2672 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ (𝐺𝑤) ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9794, 96bitrd 267 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9893, 97imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → (((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))))
9998, 29vtoclg 3239 . . . . . . . . . . . . . . . 16 ((𝐺𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
10099anabsi7 856 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
101100adantr 480 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
10291, 101eqeltrd 2688 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
103 f1ofo 6057 . . . . . . . . . . . . . . . . 17 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)–onto→ran 𝐺)
104 forn 6031 . . . . . . . . . . . . . . . . 17 (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
1055, 103, 1043syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝐹 = ran 𝐺)
106105eleq2d 2673 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝑤) ∈ ran 𝐹 ↔ (𝐺𝑤) ∈ ran 𝐺))
107106biimpar 501 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝐺𝑤) ∈ ran 𝐹)
1087adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
109 fvelrnb 6153 . . . . . . . . . . . . . . 15 (𝐹 Fn (1...𝑀) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
110108, 109syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
111107, 110mpbid 221 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤))
112102, 111reximddv 3001 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
11384, 112syldan 486 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
114 simplrl 796 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡𝑤)
115 simpr 476 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑋) → 𝑤𝑋)
11623fvmpt2 6200 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ∧ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
117115, 74, 116syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑋) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
118117eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) ↔ ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
119118biimpa 500 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤𝑋) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
120119adantlrl 752 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
121 nfcv 2751 . . . . . . . . . . . . . . . . . . 19 ((𝑌𝐹)‘𝑖)
122 nfv 1830 . . . . . . . . . . . . . . . . . . 19 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}
123 fveq1 6102 . . . . . . . . . . . . . . . . . . . . . 22 ( = ((𝑌𝐹)‘𝑖) → (𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
124123breq2d 4595 . . . . . . . . . . . . . . . . . . . . 21 ( = ((𝑌𝐹)‘𝑖) → (0 < (𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
125124rabbidv 3164 . . . . . . . . . . . . . . . . . . . 20 ( = ((𝑌𝐹)‘𝑖) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
126125eqeq2d 2620 . . . . . . . . . . . . . . . . . . 19 ( = ((𝑌𝐹)‘𝑖) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
127121, 34, 122, 126elrabf 3329 . . . . . . . . . . . . . . . . . 18 (((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
128120, 127sylib 207 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
129128simprd 478 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
130114, 129eleqtrd 2690 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
131 rabid 3095 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)} ↔ (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
132130, 131sylib 207 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
133132simprd 478 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡))
134133ex 449 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
135134reximdv 2999 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
136113, 135mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
137136ex 449 . . . . . . . . 9 (𝜑 → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
138137adantr 480 . . . . . . . 8 ((𝜑𝑡 ∈ (𝑇𝑈)) → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
13968, 138eximd 2072 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑤(𝑡𝑤𝑤𝑋) → ∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14066, 139mpd 15 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
141 nfv 1830 . . . . . . 7 𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)
142 idd 24 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14368, 141, 142exlimd 2074 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
144140, 143mpd 15 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
145144ex 449 . . . 4 (𝜑 → (𝑡 ∈ (𝑇𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14662, 145ralrimi 2940 . . 3 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
14713, 61, 146jca32 556 . 2 (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
148 feq1 5939 . . . . 5 (𝑞 = (𝑌𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌𝐹):(1...𝑀)⟶𝑄))
149 fveq1 6102 . . . . . . . . 9 (𝑞 = (𝑌𝐹) → (𝑞𝑖) = ((𝑌𝐹)‘𝑖))
150149fveq1d 6105 . . . . . . . 8 (𝑞 = (𝑌𝐹) → ((𝑞𝑖)‘𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
151150breq2d 4595 . . . . . . 7 (𝑞 = (𝑌𝐹) → (0 < ((𝑞𝑖)‘𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
152151rexbidv 3034 . . . . . 6 (𝑞 = (𝑌𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
153152ralbidv 2969 . . . . 5 (𝑞 = (𝑌𝐹) → (∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
154148, 153anbi12d 743 . . . 4 (𝑞 = (𝑌𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)) ↔ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
155154anbi2d 736 . . 3 (𝑞 = (𝑌𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))))
156155spcegv 3267 . 2 ((𝑌𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)))))
15712, 147, 156sylc 63 1 (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ⊆ wss 3540  ∪ cuni 4372   class class class wbr 4583   ↦ cmpt 4643  dom cdm 5038  ran crn 5039   ∘ ccom 5042  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   < clt 9953  ℕcn 10897  ...cfz 12197 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552 This theorem is referenced by:  stoweidlem35  38928
 Copyright terms: Public domain W3C validator