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 45406
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 7224 . . . 4 ((𝑌 Fn ran 𝐺 ∧ ran 𝐺 ∈ V) → 𝑌 ∈ V)
41, 2, 3syl2anc 583 . . 3 (𝜑𝑌 ∈ V)
5 stoweidlem27.7 . . . . 5 (𝜑𝐹:(1...𝑀)–1-1-onto→ran 𝐺)
6 f1ofn 6835 . . . . 5 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹 Fn (1...𝑀))
75, 6syl 17 . . . 4 (𝜑𝐹 Fn (1...𝑀))
8 ovex 7448 . . . 4 (1...𝑀) ∈ V
9 fnex 7224 . . . 4 ((𝐹 Fn (1...𝑀) ∧ (1...𝑀) ∈ V) → 𝐹 ∈ V)
107, 8, 9sylancl 585 . . 3 (𝜑𝐹 ∈ V)
11 coexg 7932 . . 3 ((𝑌 ∈ V ∧ 𝐹 ∈ V) → (𝑌𝐹) ∈ V)
124, 10, 11syl2anc 583 . 2 (𝜑 → (𝑌𝐹) ∈ V)
13 stoweidlem27.3 . . 3 (𝜑𝑀 ∈ ℕ)
14 f1of 6834 . . . . . 6 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺)
155, 14syl 17 . . . . 5 (𝜑𝐹:(1...𝑀)⟶ran 𝐺)
16 fnfco 6757 . . . . 5 ((𝑌 Fn ran 𝐺𝐹:(1...𝑀)⟶ran 𝐺) → (𝑌𝐹) Fn (1...𝑀))
171, 15, 16syl2anc 583 . . . 4 (𝜑 → (𝑌𝐹) Fn (1...𝑀))
18 rncoss 5970 . . . . 5 ran (𝑌𝐹) ⊆ ran 𝑌
19 fvelrnb 6954 . . . . . . . . . . 11 (𝑌 Fn ran 𝐺 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
201, 19syl 17 . . . . . . . . . 10 (𝜑 → (𝑘 ∈ ran 𝑌 ↔ ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘))
2120biimpa 476 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘)
22 stoweidlem27.10 . . . . . . . . . . . . . 14 𝑤𝜑
23 stoweidlem27.1 . . . . . . . . . . . . . . . . 17 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
24 nfmpt1 5251 . . . . . . . . . . . . . . . . 17 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2523, 24nfcxfr 2897 . . . . . . . . . . . . . . . 16 𝑤𝐺
2625nfrn 5949 . . . . . . . . . . . . . . 15 𝑤ran 𝐺
2726nfcri 2886 . . . . . . . . . . . . . 14 𝑤 𝑙 ∈ ran 𝐺
2822, 27nfan 1895 . . . . . . . . . . . . 13 𝑤(𝜑𝑙 ∈ ran 𝐺)
29 stoweidlem27.6 . . . . . . . . . . . . . . . . 17 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙)
3029ad2antrr 725 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑙)
31 simpr 484 . . . . . . . . . . . . . . . 16 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
3230, 31eleqtrd 2831 . . . . . . . . . . . . . . 15 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 nfcv 2899 . . . . . . . . . . . . . . . 16 (𝑌𝑙)
34 stoweidlem27.11 . . . . . . . . . . . . . . . 16 𝑄
35 nfv 1910 . . . . . . . . . . . . . . . 16 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}
36 fveq1 6891 . . . . . . . . . . . . . . . . . . 19 ( = (𝑌𝑙) → (𝑡) = ((𝑌𝑙)‘𝑡))
3736breq2d 5155 . . . . . . . . . . . . . . . . . 18 ( = (𝑌𝑙) → (0 < (𝑡) ↔ 0 < ((𝑌𝑙)‘𝑡)))
3837rabbidv 3436 . . . . . . . . . . . . . . . . 17 ( = (𝑌𝑙) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)})
3938eqeq2d 2739 . . . . . . . . . . . . . . . 16 ( = (𝑌𝑙) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4033, 34, 35, 39elrabf 3677 . . . . . . . . . . . . . . 15 ((𝑌𝑙) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4132, 40sylib 217 . . . . . . . . . . . . . 14 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ((𝑌𝑙) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < ((𝑌𝑙)‘𝑡)}))
4241simpld 494 . . . . . . . . . . . . 13 ((((𝜑𝑙 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (𝑌𝑙) ∈ 𝑄)
43 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → 𝑙 ∈ ran 𝐺)
4423elrnmpt 5953 . . . . . . . . . . . . . . 15 (𝑙 ∈ ran 𝐺 → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4543, 44syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑙 ∈ ran 𝐺) → (𝑙 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4643, 45mpbid 231 . . . . . . . . . . . . 13 ((𝜑𝑙 ∈ ran 𝐺) → ∃𝑤𝑋 𝑙 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4728, 42, 46r19.29af 3261 . . . . . . . . . . . 12 ((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
4847adantlr 714 . . . . . . . . . . 11 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑄)
49 eleq1 2817 . . . . . . . . . . 11 ((𝑌𝑙) = 𝑘 → ((𝑌𝑙) ∈ 𝑄𝑘𝑄))
5048, 49syl5ibcom 244 . . . . . . . . . 10 (((𝜑𝑘 ∈ ran 𝑌) ∧ 𝑙 ∈ ran 𝐺) → ((𝑌𝑙) = 𝑘𝑘𝑄))
5150reximdva 3164 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺(𝑌𝑙) = 𝑘 → ∃𝑙 ∈ ran 𝐺 𝑘𝑄))
5221, 51mpd 15 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → ∃𝑙 ∈ ran 𝐺 𝑘𝑄)
53 idd 24 . . . . . . . . . 10 (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄))
5453a1i 11 . . . . . . . . 9 ((𝜑𝑘 ∈ ran 𝑌) → (𝑙 ∈ ran 𝐺 → (𝑘𝑄𝑘𝑄)))
5554rexlimdv 3149 . . . . . . . 8 ((𝜑𝑘 ∈ ran 𝑌) → (∃𝑙 ∈ ran 𝐺 𝑘𝑄𝑘𝑄))
5652, 55mpd 15 . . . . . . 7 ((𝜑𝑘 ∈ ran 𝑌) → 𝑘𝑄)
5756ex 412 . . . . . 6 (𝜑 → (𝑘 ∈ ran 𝑌𝑘𝑄))
5857ssrdv 3985 . . . . 5 (𝜑 → ran 𝑌𝑄)
5918, 58sstrid 3990 . . . 4 (𝜑 → ran (𝑌𝐹) ⊆ 𝑄)
60 df-f 6547 . . . 4 ((𝑌𝐹):(1...𝑀)⟶𝑄 ↔ ((𝑌𝐹) Fn (1...𝑀) ∧ ran (𝑌𝐹) ⊆ 𝑄))
6117, 59, 60sylanbrc 582 . . 3 (𝜑 → (𝑌𝐹):(1...𝑀)⟶𝑄)
62 stoweidlem27.9 . . . 4 𝑡𝜑
63 nfv 1910 . . . . . . 7 𝑤 𝑡 ∈ (𝑇𝑈)
6422, 63nfan 1895 . . . . . 6 𝑤(𝜑𝑡 ∈ (𝑇𝑈))
65 nfv 1910 . . . . . 6 𝑤𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)
66 stoweidlem27.8 . . . . . . . 8 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
6766sselda 3979 . . . . . . 7 ((𝜑𝑡 ∈ (𝑇𝑈)) → 𝑡 𝑋)
68 eluni 4907 . . . . . . 7 (𝑡 𝑋 ↔ ∃𝑤(𝑡𝑤𝑤𝑋))
6967, 68sylib 217 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑤(𝑡𝑤𝑤𝑋))
7023funmpt2 6587 . . . . . . . . . . . 12 Fun 𝐺
7123dmeqi 5902 . . . . . . . . . . . . . . 15 dom 𝐺 = dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
72 stoweidlem27.2 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑄 ∈ V)
7334rabexgf 44377 . . . . . . . . . . . . . . . . . . . 20 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7574adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
7675ex 412 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤𝑋 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V))
7722, 76ralrimi 3250 . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
78 dmmptg 6241 . . . . . . . . . . . . . . . 16 (∀𝑤𝑋 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
7977, 78syl 17 . . . . . . . . . . . . . . 15 (𝜑 → dom (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) = 𝑋)
8071, 79eqtrid 2780 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐺 = 𝑋)
8180eleq2d 2815 . . . . . . . . . . . . 13 (𝜑 → (𝑤 ∈ dom 𝐺𝑤𝑋))
8281biimpar 477 . . . . . . . . . . . 12 ((𝜑𝑤𝑋) → 𝑤 ∈ dom 𝐺)
83 fvelrn 7081 . . . . . . . . . . . 12 ((Fun 𝐺𝑤 ∈ dom 𝐺) → (𝐺𝑤) ∈ ran 𝐺)
8470, 82, 83sylancr 586 . . . . . . . . . . 11 ((𝜑𝑤𝑋) → (𝐺𝑤) ∈ ran 𝐺)
8584adantrl 715 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (𝐺𝑤) ∈ ran 𝐺)
8615ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝐹:(1...𝑀)⟶ran 𝐺)
87 simprl 770 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → 𝑖 ∈ (1...𝑀))
88 fvco3 6992 . . . . . . . . . . . . . 14 ((𝐹:(1...𝑀)⟶ran 𝐺𝑖 ∈ (1...𝑀)) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
8986, 87, 88syl2anc 583 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐹𝑖)))
90 fveq2 6892 . . . . . . . . . . . . . 14 ((𝐹𝑖) = (𝐺𝑤) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9190ad2antll 728 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐹𝑖)) = (𝑌‘(𝐺𝑤)))
9289, 91eqtrd 2768 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) = (𝑌‘(𝐺𝑤)))
93 eleq1 2817 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → (𝑙 ∈ ran 𝐺 ↔ (𝐺𝑤) ∈ ran 𝐺))
9493anbi2d 629 . . . . . . . . . . . . . . . 16 (𝑙 = (𝐺𝑤) → ((𝜑𝑙 ∈ ran 𝐺) ↔ (𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺)))
95 eleq2 2818 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌𝑙) ∈ (𝐺𝑤)))
96 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (𝑙 = (𝐺𝑤) → (𝑌𝑙) = (𝑌‘(𝐺𝑤)))
9796eleq1d 2814 . . . . . . . . . . . . . . . . 17 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ (𝐺𝑤) ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9895, 97bitrd 279 . . . . . . . . . . . . . . . 16 (𝑙 = (𝐺𝑤) → ((𝑌𝑙) ∈ 𝑙 ↔ (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
9994, 98imbi12d 344 . . . . . . . . . . . . . . 15 (𝑙 = (𝐺𝑤) → (((𝜑𝑙 ∈ ran 𝐺) → (𝑌𝑙) ∈ 𝑙) ↔ ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))))
10099, 29vtoclg 3539 . . . . . . . . . . . . . 14 ((𝐺𝑤) ∈ ran 𝐺 → ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤)))
101100anabsi7 670 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
102101adantr 480 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → (𝑌‘(𝐺𝑤)) ∈ (𝐺𝑤))
10392, 102eqeltrd 2829 . . . . . . . . . . 11 (((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) ∧ (𝑖 ∈ (1...𝑀) ∧ (𝐹𝑖) = (𝐺𝑤))) → ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
104 f1ofo 6841 . . . . . . . . . . . . . . 15 (𝐹:(1...𝑀)–1-1-onto→ran 𝐺𝐹:(1...𝑀)–onto→ran 𝐺)
105 forn 6809 . . . . . . . . . . . . . . 15 (𝐹:(1...𝑀)–onto→ran 𝐺 → ran 𝐹 = ran 𝐺)
1065, 104, 1053syl 18 . . . . . . . . . . . . . 14 (𝜑 → ran 𝐹 = ran 𝐺)
107106eleq2d 2815 . . . . . . . . . . . . 13 (𝜑 → ((𝐺𝑤) ∈ ran 𝐹 ↔ (𝐺𝑤) ∈ ran 𝐺))
108107biimpar 477 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → (𝐺𝑤) ∈ ran 𝐹)
1097adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → 𝐹 Fn (1...𝑀))
110 fvelrnb 6954 . . . . . . . . . . . . 13 (𝐹 Fn (1...𝑀) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
111109, 110syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ((𝐺𝑤) ∈ ran 𝐹 ↔ ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤)))
112108, 111mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)(𝐹𝑖) = (𝐺𝑤))
113103, 112reximddv 3167 . . . . . . . . . 10 ((𝜑 ∧ (𝐺𝑤) ∈ ran 𝐺) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
11485, 113syldan 590 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤))
115 simplrl 776 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡𝑤)
116 simpr 484 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤𝑋) → 𝑤𝑋)
11723fvmpt2 7011 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ∧ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
118116, 75, 117syl2anc 583 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤𝑋) → (𝐺𝑤) = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
119118eleq2d 2815 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑤𝑋) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) ↔ ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
120119biimpa 476 . . . . . . . . . . . . . . . . 17 (((𝜑𝑤𝑋) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
121120adantlrl 719 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → ((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
122 nfcv 2899 . . . . . . . . . . . . . . . . 17 ((𝑌𝐹)‘𝑖)
123 nfv 1910 . . . . . . . . . . . . . . . . 17 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}
124 fveq1 6891 . . . . . . . . . . . . . . . . . . . 20 ( = ((𝑌𝐹)‘𝑖) → (𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
125124breq2d 5155 . . . . . . . . . . . . . . . . . . 19 ( = ((𝑌𝐹)‘𝑖) → (0 < (𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
126125rabbidv 3436 . . . . . . . . . . . . . . . . . 18 ( = ((𝑌𝐹)‘𝑖) → {𝑡𝑇 ∣ 0 < (𝑡)} = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
127126eqeq2d 2739 . . . . . . . . . . . . . . . . 17 ( = ((𝑌𝐹)‘𝑖) → (𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
128122, 34, 123, 127elrabf 3677 . . . . . . . . . . . . . . . 16 (((𝑌𝐹)‘𝑖) ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
129121, 128sylib 217 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (((𝑌𝐹)‘𝑖) ∈ 𝑄𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)}))
130129simprd 495 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑤 = {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
131115, 130eleqtrd 2831 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)})
132 rabid 3448 . . . . . . . . . . . . 13 (𝑡 ∈ {𝑡𝑇 ∣ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)} ↔ (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
133131, 132sylib 217 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → (𝑡𝑇 ∧ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
134133simprd 495 . . . . . . . . . . 11 (((𝜑 ∧ (𝑡𝑤𝑤𝑋)) ∧ ((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤)) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡))
135134ex 412 . . . . . . . . . 10 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
136135reximdv 3166 . . . . . . . . 9 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → (∃𝑖 ∈ (1...𝑀)((𝑌𝐹)‘𝑖) ∈ (𝐺𝑤) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
137114, 136mpd 15 . . . . . . . 8 ((𝜑 ∧ (𝑡𝑤𝑤𝑋)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
138137ex 412 . . . . . . 7 (𝜑 → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
139138adantr 480 . . . . . 6 ((𝜑𝑡 ∈ (𝑇𝑈)) → ((𝑡𝑤𝑤𝑋) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14064, 65, 69, 139exlimimdd 2208 . . . . 5 ((𝜑𝑡 ∈ (𝑇𝑈)) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
141140ex 412 . . . 4 (𝜑 → (𝑡 ∈ (𝑇𝑈) → ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
14262, 141ralrimi 3250 . . 3 (𝜑 → ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))
14313, 61, 142jca32 515 . 2 (𝜑 → (𝑀 ∈ ℕ ∧ ((𝑌𝐹):(1...𝑀)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡))))
144 feq1 6698 . . . . 5 (𝑞 = (𝑌𝐹) → (𝑞:(1...𝑀)⟶𝑄 ↔ (𝑌𝐹):(1...𝑀)⟶𝑄))
145 fveq1 6891 . . . . . . . . 9 (𝑞 = (𝑌𝐹) → (𝑞𝑖) = ((𝑌𝐹)‘𝑖))
146145fveq1d 6894 . . . . . . . 8 (𝑞 = (𝑌𝐹) → ((𝑞𝑖)‘𝑡) = (((𝑌𝐹)‘𝑖)‘𝑡))
147146breq2d 5155 . . . . . . 7 (𝑞 = (𝑌𝐹) → (0 < ((𝑞𝑖)‘𝑡) ↔ 0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
148147rexbidv 3174 . . . . . 6 (𝑞 = (𝑌𝐹) → (∃𝑖 ∈ (1...𝑀)0 < ((𝑞𝑖)‘𝑡) ↔ ∃𝑖 ∈ (1...𝑀)0 < (((𝑌𝐹)‘𝑖)‘𝑡)))
149148ralbidv 3173 . . . . 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 3583 . 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 395   = wceq 1534  wex 1774  wnf 1778  wcel 2099  wnfc 2879  wral 3057  wrex 3066  {crab 3428  Vcvv 3470  cdif 3942  wss 3945   cuni 4904   class class class wbr 5143  cmpt 5226  dom cdm 5673  ran crn 5674  ccom 5677  Fun wfun 6537   Fn wfn 6538  wf 6539  ontowfo 6541  1-1-ontowf1o 6542  cfv 6543  (class class class)co 7415  0cc0 11133  1c1 11134   < clt 11273  cn 12237  ...cfz 13511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7418
This theorem is referenced by:  stoweidlem35  45414
  Copyright terms: Public domain W3C validator