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 44258
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_(t0) = 0, and p > 0 on T - U. Here (𝑞𝑖) is used to represent p_(ti) 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 7167 . . . 4 ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
41, 2, 3syl2anc 584 . . 3 (𝜑𝑌 ∈ V)
5 stoweidlem27.7 . . . . 5 (𝜑𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6 f1ofn 6785 . . . . 5 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹 Fn (1...𝑀))
75, 6syl 17 . . . 4 (𝜑𝐹 Fn (1...𝑀))
8 ovex 7390 . . . 4 (1...𝑀) ∈ V
9 fnex 7167 . . . 4 ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 586 . . 3 (𝜑𝐹 ∈ V)
11 coexg 7866 . . 3 ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌𝐹) ∈ V)
124, 10, 11syl2anc 584 . 2 (𝜑 → (𝑌𝐹) ∈ V)
13 stoweidlem27.3 . . 3 (𝜑𝑀 ∈ ℕ)
14 f1of 6784 . . . . . 6 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺)
155, 14syl 17 . . . . 5 (𝜑𝐹:(1...𝑀)⟶ran 𝐺)
16 fnfco 6707 . . . . 5 ((𝑌 Fn ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌𝐹) Fn (1...𝑀))
171, 15, 16syl2anc 584 . . . 4 (𝜑 → (𝑌𝐹) Fn (1...𝑀))
18 rncoss 5927 . . . . 5 ran (𝑌𝐹) ⊆ ran 𝑌
19 fvelrnb 6903 . . . . . . . . . . 11 (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
201, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
2120biimpa 477 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘)
22 stoweidlem27.10 . . . . . . . . . . . . . 14 𝑤𝜑
23 stoweidlem27.1 . . . . . . . . . . . . . . . . 17 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
24 nfmpt1 5213 . . . . . . . . . . . . . . . . 17 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2523, 24nfcxfr 2905 . . . . . . . . . . . . . . . 16 𝑤𝐺
2625nfrn 5907 . . . . . . . . . . . . . . 15 𝑤ran 𝐺
2726nfcri 2894 . . . . . . . . . . . . . 14 𝑤 𝑙 ∈ ran 𝐺
2822, 27nfan 1902 . . . . . . . . . . . . 13 𝑤(𝜑𝑙 ∈ ran 𝐺)
29 stoweidlem27.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙)
3029ad2antrr 724 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑙)
31 simpr 485 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
3230, 31eleqtrd 2840 . . . . . . . . . . . . . . 15 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 nfcv 2907 . . . . . . . . . . . . . . . 16 (𝑌𝑙)
34 stoweidlem27.11 . . . . . . . . . . . . . . . 16 𝑄
35 nfv 1917 . . . . . . . . . . . . . . . 16 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}
36 fveq1 6841 . . . . . . . . . . . . . . . . . . 19 ( = (𝑌𝑙) → (𝑡) = ((𝑌𝑙)‘𝑡))
3736breq2d 5117 . . . . . . . . . . . . . . . . . 18 ( = (𝑌𝑙) → (0 < (𝑡) ↔ 0 < ((𝑌𝑙)‘𝑡)))
3837rabbidv 3415 . . . . . . . . . . . . . . . . 17 ( = (𝑌𝑙) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)})
3938eqeq2d 2747 . . . . . . . . . . . . . . . 16 ( = (𝑌𝑙) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4033, 34, 35, 39elrabf 3641 . . . . . . . . . . . . . . 15 ((𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4132, 40sylib 217 . . . . . . . . . . . . . 14 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4241simpld 495 . . . . . . . . . . . . 13 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑄)
43 simpr 485 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
4423elrnmpt 5911 . . . . . . . . . . . . . . 15 (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4543, 44syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4643, 45mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ran 𝐺) → ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4728, 42, 46r19.29af 3251 . . . . . . . . . . . 12 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
4847adantlr 713 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
49 eleq1 2825 . . . . . . . . . . 11 ((𝑌𝑙) = 𝑘 → ((𝑌𝑙) ∈ 𝑄𝑘𝑄))
5048, 49syl5ibcom 244 . . . . . . . . . 10 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌𝑙) = 𝑘𝑘𝑄))
5150reximdva 3165 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘𝑄))
5221, 51mpd 15 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘𝑄)
53 idd 24 . . . . . . . . . 10 (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄))
5453a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄)))
5554rexlimdv 3150 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘𝑄𝑘𝑄))
5652, 55mpd 15 . . . . . . 7 ((𝜑𝑘 ∈ ran 𝑌) → 𝑘𝑄)
5756ex 413 . . . . . 6 (𝜑 → (𝑘 ∈ ran 𝑌𝑘𝑄))
5857ssrdv 3950 . . . . 5 (𝜑 → ran 𝑌𝑄)
5918, 58sstrid 3955 . . . 4 (𝜑 → ran (𝑌𝐹) ⊆ 𝑄)
60 df-f 6500 . . . 4 ((𝑌𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌𝐹) Fn (1...𝑀) ∧ ran (𝑌𝐹) ⊆ 𝑄))
6117, 59, 60sylanbrc 583 . . 3 (𝜑 → (𝑌𝐹):(1...𝑀)⟶𝑄)
62 stoweidlem27.9 . . . 4 𝑡𝜑
63 nfv 1917 . . . . . . 7 𝑤 𝑡 ∈ (𝑇𝑈)
6422, 63nfan 1902 . . . . . 6 𝑤(𝜑𝑡 ∈ (𝑇𝑈))
65 nfv 1917 . . . . . 6 𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)
66 stoweidlem27.8 . . . . . . . 8 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
6766sselda 3944 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝑡 𝑋)
68 eluni 4868 . . . . . . 7 (𝑡 𝑋 ↔ ∃𝑤(𝑡𝑤𝑤𝑋))
6967, 68sylib 217 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤(𝑡𝑤𝑤𝑋))
7023funmpt2 6540 . . . . . . . . . . . 12 Fun 𝐺
7123dmeqi 5860 . . . . . . . . . . . . . . 15 dom 𝐺 = dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
72 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑄 ∈ V)
7334rabexgf 43219 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7574adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7675ex 413 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤𝑋 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V))
7722, 76ralrimi 3240 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
78 dmmptg 6194 . . . . . . . . . . . . . . . 16 (∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7977, 78syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
8071, 79eqtrid 2788 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑋)
8180eleq2d 2823 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ dom 𝐺𝑤𝑋))
8281biimpar 478 . . . . . . . . . . . 12 ((𝜑𝑤𝑋) → 𝑤 ∈ dom 𝐺)
83 fvelrn 7027 . . . . . . . . . . . 12 ((Fun 𝐺𝑤 ∈ dom 𝐺) → (𝐺𝑤) ∈ ran 𝐺)
8470, 82, 83sylancr 587 . . . . . . . . . . 11 ((𝜑𝑤𝑋) → (𝐺𝑤) ∈ ran 𝐺)
8584adantrl 714 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (𝐺𝑤) ∈ ran 𝐺)
8615ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87 simprl 769 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝑖 ∈ (1...𝑀))
88 fvco3 6940 . . . . . . . . . . . . . 14 ((𝐹:(1...𝑀)⟶ran 𝐺𝑖 ∈ (1...𝑀)) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
8986, 87, 88syl2anc 584 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
90 fveq2 6842 . . . . . . . . . . . . . 14 ((𝐹𝑖) = (𝐺𝑤) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9190ad2antll 727 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9289, 91eqtrd 2776 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐺𝑤)))
93 eleq1 2825 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺𝑤) ∈ ran 𝐺))
9493anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑙 = (𝐺𝑤) → ((𝜑𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺)))
95 eleq2 2826 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌𝑙) ∈ (𝐺𝑤)))
96 fveq2 6842 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → (𝑌𝑙) = (𝑌‘(𝐺𝑤)))
9796eleq1d 2822 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ (𝐺𝑤) ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9895, 97bitrd 278 . . . . . . . . . . . . . . . 16 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9994, 98imbi12d 344 . . . . . . . . . . . . . . 15 (𝑙 = (𝐺𝑤) → (((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))))
10099, 29vtoclg 3525 . . . . . . . . . . . . . 14 ((𝐺𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
101100anabsi7 669 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
102101adantr 481 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
10392, 102eqeltrd 2838 . . . . . . . . . . 11 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
104 f1ofo 6791 . . . . . . . . . . . . . . 15 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)–onto→ran 𝐺)
105 forn 6759 . . . . . . . . . . . . . . 15 (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
1065, 104, 1053syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐹 = ran 𝐺)
107106eleq2d 2823 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝑤) ∈ ran 𝐹 ↔ (𝐺𝑤) ∈ ran 𝐺))
108107biimpar 478 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝐺𝑤) ∈ ran 𝐹)
1097adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110 fvelrnb 6903 . . . . . . . . . . . . 13 (𝐹 Fn (1...𝑀) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
111109, 110syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
112108, 111mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤))
113103, 112reximddv 3168 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
11485, 113syldan 591 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
115 simplrl 775 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡𝑤)
116 simpr 485 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → 𝑤𝑋)
11723fvmpt2 6959 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ∧ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
118116, 75, 117syl2anc 584 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑋) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
119118eleq2d 2823 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑋) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) ↔ ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
120119biimpa 477 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝑋) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
121120adantlrl 718 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
122 nfcv 2907 . . . . . . . . . . . . . . . . 17 ((𝑌𝐹)‘𝑖)
123 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}
124 fveq1 6841 . . . . . . . . . . . . . . . . . . . 20 ( = ((𝑌𝐹)‘𝑖) → (𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
125124breq2d 5117 . . . . . . . . . . . . . . . . . . 19 ( = ((𝑌𝐹)‘𝑖) → (0 < (𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
126125rabbidv 3415 . . . . . . . . . . . . . . . . . 18 ( = ((𝑌𝐹)‘𝑖) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
127126eqeq2d 2747 . . . . . . . . . . . . . . . . 17 ( = ((𝑌𝐹)‘𝑖) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
128122, 34, 123, 127elrabf 3641 . . . . . . . . . . . . . . . 16 (((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
129121, 128sylib 217 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
130129simprd 496 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
131115, 130eleqtrd 2840 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
132 rabid 3427 . . . . . . . . . . . . 13 (𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)} ↔ (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
133131, 132sylib 217 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
134133simprd 496 . . . . . . . . . . 11 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡))
135134ex 413 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
136135reximdv 3167 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
137114, 136mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
138137ex 413 . . . . . . 7 (𝜑 → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
139138adantr 481 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14064, 65, 69, 139exlimimdd 2212 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
141140ex 413 . . . 4 (𝜑 → (𝑡 ∈ (𝑇𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14262, 141ralrimi 3240 . . 3 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
14313, 61, 142jca32 516 . 2 (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
144 feq1 6649 . . . . 5 (𝑞 = (𝑌𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌𝐹):(1...𝑀)⟶𝑄))
145 fveq1 6841 . . . . . . . . 9 (𝑞 = (𝑌𝐹) → (𝑞𝑖) = ((𝑌𝐹)‘𝑖))
146145fveq1d 6844 . . . . . . . 8 (𝑞 = (𝑌𝐹) → ((𝑞𝑖)‘𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
147146breq2d 5117 . . . . . . 7 (𝑞 = (𝑌𝐹) → (0 < ((𝑞𝑖)‘𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
148147rexbidv 3175 . . . . . 6 (𝑞 = (𝑌𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
149148ralbidv 3174 . . . . 5 (𝑞 = (𝑌𝐹) → (∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
150144, 149anbi12d 631 . . . 4 (𝑞 = (𝑌𝐹) → ((𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)) ↔ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
151150anbi2d 629 . . 3 (𝑞 = (𝑌𝐹) → ((𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))) ↔ (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))))
152151spcegv 3556 . 2 ((𝑌𝐹) ∈ V → ((𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))) → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡)))))
15312, 143, 152sylc 65 1 (𝜑 → ∃𝑞(𝑀 ∈ ℕ ∧ (𝑞:(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2887  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  cdif 3907  wss 3910   cuni 4865   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  ccom 5637  Fun wfun 6490   Fn wfn 6491  wf 6492  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496  (class class class)co 7357  0cc0 11051  1c1 11052   < clt 11189  cn 12153  ...cfz 13424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360
This theorem is referenced by:  stoweidlem35  44266
  Copyright terms: Public domain W3C validator