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

Theorem stoweidlem35 40015
Description: This lemma is used to prove the existence of a function p as in Lemma 1 of [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
stoweidlem35.1 𝑡𝜑
stoweidlem35.2 𝑤𝜑
stoweidlem35.3 𝜑
stoweidlem35.4 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
stoweidlem35.5 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
stoweidlem35.6 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
stoweidlem35.7 (𝜑𝐴 ∈ V)
stoweidlem35.8 (𝜑𝑋 ∈ Fin)
stoweidlem35.9 (𝜑𝑋𝑊)
stoweidlem35.10 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
stoweidlem35.11 (𝜑 → (𝑇𝑈) ≠ ∅)
Assertion
Ref Expression
stoweidlem35 (𝜑 → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
Distinct variable groups:   ,𝑖,𝑡,𝑤   𝑖,𝑚,𝑞,𝑡   𝑖,𝐺   𝑤,𝑄   𝑇,,𝑤   𝑈,𝑞   𝜑,𝑖,𝑚   𝐴,,𝑡   ,𝑋,𝑖,𝑡,𝑤   𝑤,𝑚   𝑚,𝐺   𝑄,𝑞   𝑇,𝑞   𝑡,𝑍   𝑤,𝑈
Allowed substitution hints:   𝜑(𝑤,𝑡,,𝑞)   𝐴(𝑤,𝑖,𝑚,𝑞)   𝑄(𝑡,,𝑖,𝑚)   𝑇(𝑡,𝑖,𝑚)   𝑈(𝑡,,𝑖,𝑚)   𝐺(𝑤,𝑡,,𝑞)   𝐽(𝑤,𝑡,,𝑖,𝑚,𝑞)   𝑊(𝑤,𝑡,,𝑖,𝑚,𝑞)   𝑋(𝑚,𝑞)   𝑍(𝑤,,𝑖,𝑚,𝑞)

Proof of Theorem stoweidlem35
Dummy variables 𝑘 𝑓 𝑔 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem35.8 . . . . . . . . . 10 (𝜑𝑋 ∈ Fin)
2 stoweidlem35.6 . . . . . . . . . . 11 𝐺 = (𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
32rnmptfi 39167 . . . . . . . . . 10 (𝑋 ∈ Fin → ran 𝐺 ∈ Fin)
41, 3syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
5 fnchoice 39008 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
65adantl 482 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
7 simprl 793 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺)
8 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝜑
9 nfmpt1 4738 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
102, 9nfcxfr 2760 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤𝐺
1110nfrn 5357 . . . . . . . . . . . . . . . . . . . . . 22 𝑤ran 𝐺
1211nfcri 2756 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑘 ∈ ran 𝐺
138, 12nfan 1826 . . . . . . . . . . . . . . . . . . . 20 𝑤(𝜑𝑘 ∈ ran 𝐺)
14 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋𝑊)
1514sselda 3595 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑋) → 𝑤𝑊)
16 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
1715, 16syl6eleq 2709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑋) → 𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
18 rabid 3111 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
1917, 18sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑋) → (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2019simprd 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑋) → ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)})
21 df-rex 2915 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2220, 21sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑋) → ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
23 rabid 3111 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2423exbii 1772 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2522, 24sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2625adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
27 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝜑
28 nfv 1841 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝑋
2927, 28nfan 1826 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑤𝑋)
30 nfrab1 3117 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3130nfeq2 2777 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3229, 31nfan 1826 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 eleq2 2688 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → (𝑘 ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
3433biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3534adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3632, 35eximd 2083 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ∃ 𝑘))
3726, 36mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
3837adantllr 754 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
392elrnmpt 5361 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4039ibi 256 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ran 𝐺 → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4140adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ran 𝐺) → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4213, 38, 41r19.29af 3072 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ran 𝐺) → ∃ 𝑘)
43 n0 3923 . . . . . . . . . . . . . . . . . . 19 (𝑘 ≠ ∅ ↔ ∃ 𝑘)
4442, 43sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
4544adantlr 750 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
46 simplrr 800 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))
47 neeq1 2853 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅))
48 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑘 → (𝑔𝑙) = (𝑔𝑘))
4948eleq1d 2684 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑙))
50 eleq2 2688 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑘) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5149, 50bitrd 268 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5247, 51imbi12d 334 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘)))
5352rspccva 3303 . . . . . . . . . . . . . . . . . 18 ((∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5446, 53sylancom 700 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5545, 54mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
5655ralrimiva 2963 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘)
57 fveq2 6178 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑔𝑘) = (𝑔𝑙))
5857eleq1d 2684 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑘))
59 eleq2 2688 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑙) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6058, 59bitrd 268 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6160cbvralv 3166 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
6256, 61sylib 208 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
637, 62jca 554 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6463ex 450 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6564adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6665eximdv 1844 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
676, 66mpd 15 . . . . . . . . 9 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
684, 67mpdan 701 . . . . . . . 8 (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6968ralrimivw 2964 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
70 stoweidlem35.10 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
71 stoweidlem35.11 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ≠ ∅)
72 ssn0 3967 . . . . . . . . . . . . 13 (((𝑇𝑈) ⊆ 𝑋 ∧ (𝑇𝑈) ≠ ∅) → 𝑋 ≠ ∅)
7370, 71, 72syl2anc 692 . . . . . . . . . . . 12 (𝜑 𝑋 ≠ ∅)
7473neneqd 2796 . . . . . . . . . . 11 (𝜑 → ¬ 𝑋 = ∅)
75 unieq 4435 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑋 = ∅)
76 uni0 4456 . . . . . . . . . . . 12 ∅ = ∅
7775, 76syl6eq 2670 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑋 = ∅)
7874, 77nsyl 135 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
79 dm0rn0 5331 . . . . . . . . . . 11 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
80 stoweidlem35.4 . . . . . . . . . . . . . . . . . 18 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
81 stoweidlem35.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
8280, 81rabexd 4805 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ V)
83 nfrab1 3117 . . . . . . . . . . . . . . . . . . 19 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
8480, 83nfcxfr 2760 . . . . . . . . . . . . . . . . . 18 𝑄
8584rabexgf 39003 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8682, 85syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8786adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
888, 87, 2fmptdf 6373 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋⟶V)
89 dffn2 6034 . . . . . . . . . . . . . 14 (𝐺 Fn 𝑋𝐺:𝑋⟶V)
9088, 89sylibr 224 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
91 fndm 5978 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋)
9290, 91syl 17 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝑋)
9392eqeq1d 2622 . . . . . . . . . . 11 (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅))
9479, 93syl5bbr 274 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅))
9578, 94mtbird 315 . . . . . . . . 9 (𝜑 → ¬ ran 𝐺 = ∅)
96 fz1f1o 14422 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
974, 96syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9897ord 392 . . . . . . . . 9 (𝜑 → (¬ ran 𝐺 = ∅ → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9995, 98mpd 15 . . . . . . . 8 (𝜑 → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
100 oveq2 6643 . . . . . . . . . . 11 (𝑚 = (#‘ran 𝐺) → (1...𝑚) = (1...(#‘ran 𝐺)))
101 f1oeq2 6115 . . . . . . . . . . 11 ((1...𝑚) = (1...(#‘ran 𝐺)) → (𝑓:(1...𝑚)–1-1-onto→ran 𝐺𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
102100, 101syl 17 . . . . . . . . . 10 (𝑚 = (#‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran 𝐺𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
103102exbidv 1848 . . . . . . . . 9 (𝑚 = (#‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺 ↔ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
104103rspcev 3304 . . . . . . . 8 (((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
10599, 104syl 17 . . . . . . 7 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
106 r19.29 3068 . . . . . . 7 ((∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
10769, 105, 106syl2anc 692 . . . . . 6 (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
108 eeanv 2180 . . . . . . . . 9 (∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
109108biimpri 218 . . . . . . . 8 ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
110109a1i 11 . . . . . . 7 (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
111110reximdv 3013 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
112107, 111mpd 15 . . . . 5 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
113 df-rex 2915 . . . . 5 (∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
114112, 113sylib 208 . . . 4 (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
115 ax-5 1837 . . . . . . . . 9 (𝑚 ∈ ℕ → ∀𝑔 𝑚 ∈ ℕ)
116 19.29 1799 . . . . . . . . 9 ((∀𝑔 𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
117115, 116sylan 488 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
118 ax-5 1837 . . . . . . . . . 10 (𝑚 ∈ ℕ → ∀𝑓 𝑚 ∈ ℕ)
119 19.29 1799 . . . . . . . . . 10 ((∀𝑓 𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
120118, 119sylan 488 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
121120eximi 1760 . . . . . . . 8 (∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
122117, 121syl 17 . . . . . . 7 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
123 df-3an 1038 . . . . . . . . 9 ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
124123anbi2i 729 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1251242exbii 1773 . . . . . . 7 (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
126122, 125sylibr 224 . . . . . 6 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
127126a1i 11 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
128127eximdv 1844 . . . 4 (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
129114, 128mpd 15 . . 3 (𝜑 → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
13082adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑄 ∈ V)
131 simprl 793 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑚 ∈ ℕ)
132 simprr1 1107 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑔 Fn ran 𝐺)
133 elex 3207 . . . . . . . . 9 (ran 𝐺 ∈ Fin → ran 𝐺 ∈ V)
1344, 133syl 17 . . . . . . . 8 (𝜑 → ran 𝐺 ∈ V)
135134adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ran 𝐺 ∈ V)
136 simprr2 1108 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
13751rspccva 3303 . . . . . . . 8 ((∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
138136, 137sylan 488 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
139 simprr3 1109 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
14070adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → (𝑇𝑈) ⊆ 𝑋)
141 stoweidlem35.1 . . . . . . . 8 𝑡𝜑
142 nfv 1841 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
143 nfcv 2762 . . . . . . . . . . 11 𝑡𝑔
144 nfcv 2762 . . . . . . . . . . . . . 14 𝑡𝑋
145 nfrab1 3117 . . . . . . . . . . . . . . . 16 𝑡{𝑡𝑇 ∣ 0 < (𝑡)}
146145nfeq2 2777 . . . . . . . . . . . . . . 15 𝑡 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}
147 nfv 1841 . . . . . . . . . . . . . . . . . 18 𝑡(𝑍) = 0
148 nfra1 2938 . . . . . . . . . . . . . . . . . 18 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
149147, 148nfan 1826 . . . . . . . . . . . . . . . . 17 𝑡((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))
150 nfcv 2762 . . . . . . . . . . . . . . . . 17 𝑡𝐴
151149, 150nfrab 3118 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
15280, 151nfcxfr 2760 . . . . . . . . . . . . . . 15 𝑡𝑄
153146, 152nfrab 3118 . . . . . . . . . . . . . 14 𝑡{𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
154144, 153nfmpt 4737 . . . . . . . . . . . . 13 𝑡(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
1552, 154nfcxfr 2760 . . . . . . . . . . . 12 𝑡𝐺
156155nfrn 5357 . . . . . . . . . . 11 𝑡ran 𝐺
157143, 156nffn 5975 . . . . . . . . . 10 𝑡 𝑔 Fn ran 𝐺
158 nfv 1841 . . . . . . . . . . 11 𝑡(𝑔𝑙) ∈ 𝑙
159156, 158nfral 2942 . . . . . . . . . 10 𝑡𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
160 nfcv 2762 . . . . . . . . . . 11 𝑡𝑓
161 nfcv 2762 . . . . . . . . . . 11 𝑡(1...𝑚)
162160, 161, 156nff1o 6122 . . . . . . . . . 10 𝑡 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
163157, 159, 162nf3an 1829 . . . . . . . . 9 𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
164142, 163nfan 1826 . . . . . . . 8 𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
165141, 164nfan 1826 . . . . . . 7 𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
166 nfv 1841 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
167 nfcv 2762 . . . . . . . . . . 11 𝑤𝑔
168167, 11nffn 5975 . . . . . . . . . 10 𝑤 𝑔 Fn ran 𝐺
169 nfv 1841 . . . . . . . . . . 11 𝑤(𝑔𝑙) ∈ 𝑙
17011, 169nfral 2942 . . . . . . . . . 10 𝑤𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
171 nfcv 2762 . . . . . . . . . . 11 𝑤𝑓
172 nfcv 2762 . . . . . . . . . . 11 𝑤(1...𝑚)
173171, 172, 11nff1o 6122 . . . . . . . . . 10 𝑤 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
174168, 170, 173nf3an 1829 . . . . . . . . 9 𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
175166, 174nfan 1826 . . . . . . . 8 𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
1768, 175nfan 1826 . . . . . . 7 𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1772, 130, 131, 132, 135, 138, 139, 140, 165, 176, 84stoweidlem27 40007 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
178177ex 450 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
1791782eximdv 1846 . . . 4 (𝜑 → (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
180179eximdv 1844 . . 3 (𝜑 → (∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
181129, 180mpd 15 . 2 (𝜑 → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
182 id 22 . . . 4 (∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
183182exlimivv 1858 . . 3 (∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
184183eximi 1760 . 2 (∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
185181, 184syl 17 1 (𝜑 → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036  wal 1479   = wceq 1481  wex 1702  wnf 1706  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  wss 3567  c0 3907   cuni 4427   class class class wbr 4644  cmpt 4720  dom cdm 5104  ran crn 5105   Fn wfn 5871  wf 5872  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  Fincfn 7940  0cc0 9921  1c1 9922   < clt 10059  cle 10060  cn 11005  ...cfz 12311  #chash 13100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-n0 11278  df-z 11363  df-uz 11673  df-fz 12312  df-hash 13101
This theorem is referenced by:  stoweidlem53  40033
  Copyright terms: Public domain W3C validator