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

Theorem stoweidlem27 38724
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 6364 . . . 4 ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
41, 2, 3syl2anc 690 . . 3 (𝜑𝑌 ∈ V)
5 stoweidlem27.7 . . . . 5 (𝜑𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6 f1ofn 6036 . . . . 5 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹 Fn (1...𝑀))
75, 6syl 17 . . . 4 (𝜑𝐹 Fn (1...𝑀))
8 ovex 6555 . . . 4 (1...𝑀) ∈ V
9 fnex 6364 . . . 4 ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 692 . . 3 (𝜑𝐹 ∈ V)
11 coexg 6987 . . 3 ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌𝐹) ∈ V)
124, 10, 11syl2anc 690 . 2 (𝜑 → (𝑌𝐹) ∈ V)
13 stoweidlem27.3 . . 3 (𝜑𝑀 ∈ ℕ)
14 f1of 6035 . . . . . 6 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺)
155, 14syl 17 . . . . 5 (𝜑𝐹:(1...𝑀)⟶ran 𝐺)
16 fnfco 5967 . . . . 5 ((𝑌 Fn ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌𝐹) Fn (1...𝑀))
171, 15, 16syl2anc 690 . . . 4 (𝜑 → (𝑌𝐹) Fn (1...𝑀))
18 rncoss 5294 . . . . 5 ran (𝑌𝐹) ⊆ ran 𝑌
19 fvelrnb 6138 . . . . . . . . . . 11 (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
201, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
2120biimpa 499 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘)
22 stoweidlem27.10 . . . . . . . . . . . . . 14 𝑤𝜑
23 stoweidlem27.1 . . . . . . . . . . . . . . . . 17 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
24 nfmpt1 4669 . . . . . . . . . . . . . . . . 17 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2523, 24nfcxfr 2748 . . . . . . . . . . . . . . . 16 𝑤𝐺
2625nfrn 5276 . . . . . . . . . . . . . . 15 𝑤ran 𝐺
2726nfcri 2744 . . . . . . . . . . . . . 14 𝑤 𝑙 ∈ ran 𝐺
2822, 27nfan 1815 . . . . . . . . . . . . 13 𝑤(𝜑𝑙 ∈ ran 𝐺)
29 stoweidlem27.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙)
3029ad2antrr 757 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑙)
31 simpr 475 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
3230, 31eleqtrd 2689 . . . . . . . . . . . . . . 15 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 nfcv 2750 . . . . . . . . . . . . . . . 16 (𝑌𝑙)
34 stoweidlem27.11 . . . . . . . . . . . . . . . 16 𝑄
35 nfv 1829 . . . . . . . . . . . . . . . 16 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}
36 fveq1 6087 . . . . . . . . . . . . . . . . . . 19 ( = (𝑌𝑙) → (𝑡) = ((𝑌𝑙)‘𝑡))
3736breq2d 4589 . . . . . . . . . . . . . . . . . 18 ( = (𝑌𝑙) → (0 < (𝑡) ↔ 0 < ((𝑌𝑙)‘𝑡)))
3837rabbidv 3163 . . . . . . . . . . . . . . . . 17 ( = (𝑌𝑙) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)})
3938eqeq2d 2619 . . . . . . . . . . . . . . . 16 ( = (𝑌𝑙) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4033, 34, 35, 39elrabf 3328 . . . . . . . . . . . . . . 15 ((𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4132, 40sylib 206 . . . . . . . . . . . . . 14 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4241simpld 473 . . . . . . . . . . . . 13 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑄)
43 simpr 475 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
4423elrnmpt 5280 . . . . . . . . . . . . . . 15 (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4543, 44syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4643, 45mpbid 220 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ran 𝐺) → ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4728, 42, 46r19.29af 3057 . . . . . . . . . . . 12 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
4847adantlr 746 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
49 eleq1 2675 . . . . . . . . . . 11 ((𝑌𝑙) = 𝑘 → ((𝑌𝑙) ∈ 𝑄𝑘𝑄))
5048, 49syl5ibcom 233 . . . . . . . . . 10 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌𝑙) = 𝑘𝑘𝑄))
5150reximdva 2999 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘𝑄))
5221, 51mpd 15 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘𝑄)
53 idd 24 . . . . . . . . . 10 (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄))
5453a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄)))
5554rexlimdv 3011 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘𝑄𝑘𝑄))
5652, 55mpd 15 . . . . . . 7 ((𝜑𝑘 ∈ ran 𝑌) → 𝑘𝑄)
5756ex 448 . . . . . 6 (𝜑 → (𝑘 ∈ ran 𝑌𝑘𝑄))
5857ssrdv 3573 . . . . 5 (𝜑 → ran 𝑌𝑄)
5918, 58syl5ss 3578 . . . 4 (𝜑 → ran (𝑌𝐹) ⊆ 𝑄)
60 df-f 5794 . . . 4 ((𝑌𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌𝐹) Fn (1...𝑀) ∧ ran (𝑌𝐹) ⊆ 𝑄))
6117, 59, 60sylanbrc 694 . . 3 (𝜑 → (𝑌𝐹):(1...𝑀)⟶𝑄)
62 stoweidlem27.9 . . . 4 𝑡𝜑
63 stoweidlem27.8 . . . . . . . . 9 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
6463sselda 3567 . . . . . . . 8 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝑡 𝑋)
65 eluni 4369 . . . . . . . 8 (𝑡 𝑋 ↔ ∃𝑤(𝑡𝑤𝑤𝑋))
6664, 65sylib 206 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤(𝑡𝑤𝑤𝑋))
67 nfv 1829 . . . . . . . . 9 𝑤 𝑡 ∈ (𝑇𝑈)
6822, 67nfan 1815 . . . . . . . 8 𝑤(𝜑𝑡 ∈ (𝑇𝑈))
6923funmpt2 5827 . . . . . . . . . . . . . 14 Fun 𝐺
7023dmeqi 5234 . . . . . . . . . . . . . . . . 17 dom 𝐺 = dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
71 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑄 ∈ V)
7234rabexgf 38009 . . . . . . . . . . . . . . . . . . . . . 22 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7473adantr 479 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7574ex 448 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑤𝑋 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V))
7622, 75ralrimi 2939 . . . . . . . . . . . . . . . . . 18 (𝜑 → ∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
77 dmmptg 5535 . . . . . . . . . . . . . . . . . 18 (∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7876, 77syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7970, 78syl5eq 2655 . . . . . . . . . . . . . . . 16 (𝜑 → dom 𝐺 = 𝑋)
8079eleq2d 2672 . . . . . . . . . . . . . . 15 (𝜑 → (𝑤 ∈ dom 𝐺𝑤𝑋))
8180biimpar 500 . . . . . . . . . . . . . 14 ((𝜑𝑤𝑋) → 𝑤 ∈ dom 𝐺)
82 fvelrn 6245 . . . . . . . . . . . . . 14 ((Fun 𝐺𝑤 ∈ dom 𝐺) → (𝐺𝑤) ∈ ran 𝐺)
8369, 81, 82sylancr 693 . . . . . . . . . . . . 13 ((𝜑𝑤𝑋) → (𝐺𝑤) ∈ ran 𝐺)
8483adantrl 747 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (𝐺𝑤) ∈ ran 𝐺)
8515ad2antrr 757 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
86 simprl 789 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝑖 ∈ (1...𝑀))
87 fvco3 6170 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑀)⟶ran 𝐺𝑖 ∈ (1...𝑀)) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
8885, 86, 87syl2anc 690 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
89 fveq2 6088 . . . . . . . . . . . . . . . 16 ((𝐹𝑖) = (𝐺𝑤) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9089ad2antll 760 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9188, 90eqtrd 2643 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐺𝑤)))
92 eleq1 2675 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺𝑤) ∈ ran 𝐺))
9392anbi2d 735 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → ((𝜑𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺)))
94 eleq2 2676 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌𝑙) ∈ (𝐺𝑤)))
95 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = (𝐺𝑤) → (𝑌𝑙) = (𝑌‘(𝐺𝑤)))
9695eleq1d 2671 . . . . . . . . . . . . . . . . . . 19 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ (𝐺𝑤) ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9794, 96bitrd 266 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9893, 97imbi12d 332 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → (((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))))
9998, 29vtoclg 3238 . . . . . . . . . . . . . . . 16 ((𝐺𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
10099anabsi7 855 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
101100adantr 479 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
10291, 101eqeltrd 2687 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
103 f1ofo 6042 . . . . . . . . . . . . . . . . 17 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)–onto→ran 𝐺)
104 forn 6016 . . . . . . . . . . . . . . . . 17 (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
1055, 103, 1043syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → ran 𝐹 = ran 𝐺)
106105eleq2d 2672 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐺𝑤) ∈ ran 𝐹 ↔ (𝐺𝑤) ∈ ran 𝐺))
107106biimpar 500 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝐺𝑤) ∈ ran 𝐹)
1087adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
109 fvelrnb 6138 . . . . . . . . . . . . . . 15 (𝐹 Fn (1...𝑀) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
110108, 109syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
111107, 110mpbid 220 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤))
112102, 111reximddv 3000 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
11384, 112syldan 485 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
114 simplrl 795 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡𝑤)
115 simpr 475 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤𝑋) → 𝑤𝑋)
11623fvmpt2 6185 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ∧ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
117115, 74, 116syl2anc 690 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤𝑋) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
118117eleq2d 2672 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) ↔ ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
119118biimpa 499 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑤𝑋) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
120119adantlrl 751 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
121 nfcv 2750 . . . . . . . . . . . . . . . . . . 19 ((𝑌𝐹)‘𝑖)
122 nfv 1829 . . . . . . . . . . . . . . . . . . 19 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}
123 fveq1 6087 . . . . . . . . . . . . . . . . . . . . . 22 ( = ((𝑌𝐹)‘𝑖) → (𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
124123breq2d 4589 . . . . . . . . . . . . . . . . . . . . 21 ( = ((𝑌𝐹)‘𝑖) → (0 < (𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
125124rabbidv 3163 . . . . . . . . . . . . . . . . . . . 20 ( = ((𝑌𝐹)‘𝑖) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
126125eqeq2d 2619 . . . . . . . . . . . . . . . . . . 19 ( = ((𝑌𝐹)‘𝑖) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
127121, 34, 122, 126elrabf 3328 . . . . . . . . . . . . . . . . . 18 (((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
128120, 127sylib 206 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
129128simprd 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
130114, 129eleqtrd 2689 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
131 rabid 3094 . . . . . . . . . . . . . . 15 (𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)} ↔ (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
132130, 131sylib 206 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
133132simprd 477 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡))
134133ex 448 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
135134reximdv 2998 . . . . . . . . . . 11 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
136113, 135mpd 15 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
137136ex 448 . . . . . . . . 9 (𝜑 → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
138137adantr 479 . . . . . . . 8 ((𝜑𝑡 ∈ (𝑇𝑈)) → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
13968, 138eximd 2070 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑤(𝑡𝑤𝑤𝑋) → ∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14066, 139mpd 15 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
141 nfv 1829 . . . . . . 7 𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)
142 idd 24 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14368, 141, 142exlimd 2072 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → (∃𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
144140, 143mpd 15 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
145144ex 448 . . . 4 (𝜑 → (𝑡 ∈ (𝑇𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14662, 145ralrimi 2939 . . 3 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
14713, 61, 146jca32 555 . 2 (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
148 feq1 5925 . . . . 5 (𝑞 = (𝑌𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌𝐹):(1...𝑀)⟶𝑄))
149 fveq1 6087 . . . . . . . . 9 (𝑞 = (𝑌𝐹) → (𝑞𝑖) = ((𝑌𝐹)‘𝑖))
150149fveq1d 6090 . . . . . . . 8 (𝑞 = (𝑌𝐹) → ((𝑞𝑖)‘𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
151150breq2d 4589 . . . . . . 7 (𝑞 = (𝑌𝐹) → (0 < ((𝑞𝑖)‘𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
152151rexbidv 3033 . . . . . 6 (𝑞 = (𝑌𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
153152ralbidv 2968 . . . . 5 (𝑞 = (𝑌𝐹) → (∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
154148, 153anbi12d 742 . . . 4 (𝑞 = (𝑌𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)) ↔ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
155154anbi2d 735 . . 3 (𝑞 = (𝑌𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))))
156155spcegv 3266 . 2 ((𝑌𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)))))
15712, 147, 156sylc 62 1 (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wex 1694  wnf 1698  wcel 1976  wnfc 2737  wral 2895  wrex 2896  {crab 2899  Vcvv 3172  cdif 3536  wss 3539   cuni 4366   class class class wbr 4577  cmpt 4637  dom cdm 5028  ran crn 5029  ccom 5032  Fun wfun 5784   Fn wfn 5785  wf 5786  ontowfo 5788  1-1-ontowf1o 5789  cfv 5790  (class class class)co 6527  0cc0 9792  1c1 9793   < clt 9930  cn 10867  ...cfz 12152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-ov 6530
This theorem is referenced by:  stoweidlem35  38732
  Copyright terms: Public domain W3C validator