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 41816
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_(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
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 40920 . . . . . . . . . 10 (𝑋 ∈ Fin → ran 𝐺 ∈ Fin)
41, 3syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
5 fnchoice 40777 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
65adantl 482 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
7 simprl 767 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺)
8 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝜑
9 nfmpt1 5052 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
102, 9nfcxfr 2945 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤𝐺
1110nfrn 5698 . . . . . . . . . . . . . . . . . . . . . 22 𝑤ran 𝐺
1211nfcri 2941 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑘 ∈ ran 𝐺
138, 12nfan 1879 . . . . . . . . . . . . . . . . . . . 20 𝑤(𝜑𝑘 ∈ ran 𝐺)
14 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋𝑊)
1514sselda 3884 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑋) → 𝑤𝑊)
16 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
1715, 16syl6eleq 2891 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑋) → 𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
18 rabid 3334 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
1917, 18sylib 219 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑋) → (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2019simprd 496 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑋) → ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)})
21 df-rex 3109 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2220, 21sylib 219 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑋) → ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
23 rabid 3334 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2423exbii 1827 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2522, 24sylibr 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2625adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
27 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝜑
28 nfv 1890 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝑋
2927, 28nfan 1879 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑤𝑋)
30 nfrab1 3341 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3130nfeq2 2962 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3229, 31nfan 1879 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 eleq2 2869 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → (𝑘 ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
3433biimprd 249 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3534adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3632, 35eximd 2179 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ∃ 𝑘))
3726, 36mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
3837adantllr 715 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
392elrnmpt 5702 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4039ibi 268 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ran 𝐺 → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4140adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ran 𝐺) → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4213, 38, 41r19.29af 3289 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ran 𝐺) → ∃ 𝑘)
43 n0 4224 . . . . . . . . . . . . . . . . . . 19 (𝑘 ≠ ∅ ↔ ∃ 𝑘)
4442, 43sylibr 235 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
4544adantlr 711 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
46 simplrr 774 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))
47 neeq1 3044 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅))
48 fveq2 6530 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑘 → (𝑔𝑙) = (𝑔𝑘))
4948eleq1d 2865 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑙))
50 eleq2 2869 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑘) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5149, 50bitrd 280 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5247, 51imbi12d 346 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘)))
5352rspccva 3553 . . . . . . . . . . . . . . . . . 18 ((∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5446, 53sylancom 588 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5545, 54mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
5655ralrimiva 3147 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘)
57 fveq2 6530 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑔𝑘) = (𝑔𝑙))
5857eleq1d 2865 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑘))
59 eleq2 2869 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑙) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6058, 59bitrd 280 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6160cbvralv 3400 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
6256, 61sylib 219 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
637, 62jca 512 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6463ex 413 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6564adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6665eximdv 1893 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
676, 66mpd 15 . . . . . . . . 9 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
684, 67mpdan 683 . . . . . . . 8 (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6968ralrimivw 3148 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
70 stoweidlem35.10 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
71 stoweidlem35.11 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ≠ ∅)
72 ssn0 4268 . . . . . . . . . . . . 13 (((𝑇𝑈) ⊆ 𝑋 ∧ (𝑇𝑈) ≠ ∅) → 𝑋 ≠ ∅)
7370, 71, 72syl2anc 584 . . . . . . . . . . . 12 (𝜑 𝑋 ≠ ∅)
7473neneqd 2987 . . . . . . . . . . 11 (𝜑 → ¬ 𝑋 = ∅)
75 unieq 4747 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑋 = ∅)
76 uni0 4766 . . . . . . . . . . . 12 ∅ = ∅
7775, 76syl6eq 2845 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑋 = ∅)
7874, 77nsyl 142 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
79 dm0rn0 5671 . . . . . . . . . . 11 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
80 stoweidlem35.4 . . . . . . . . . . . . . . . . . 18 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
81 stoweidlem35.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
8280, 81rabexd 5120 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ V)
83 nfrab1 3341 . . . . . . . . . . . . . . . . . . 19 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
8480, 83nfcxfr 2945 . . . . . . . . . . . . . . . . . 18 𝑄
8584rabexgf 40772 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8682, 85syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8786adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
888, 87, 2fmptdf 6735 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋⟶V)
89 dffn2 6376 . . . . . . . . . . . . . 14 (𝐺 Fn 𝑋𝐺:𝑋⟶V)
9088, 89sylibr 235 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
91 fndm 6317 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋)
9290, 91syl 17 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝑋)
9392eqeq1d 2795 . . . . . . . . . . 11 (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅))
9479, 93syl5bbr 286 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅))
9578, 94mtbird 326 . . . . . . . . 9 (𝜑 → ¬ ran 𝐺 = ∅)
96 fz1f1o 14888 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
974, 96syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
9897ord 859 . . . . . . . . 9 (𝜑 → (¬ ran 𝐺 = ∅ → ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
9995, 98mpd 15 . . . . . . . 8 (𝜑 → ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
100 oveq2 7015 . . . . . . . . . . 11 (𝑚 = (♯‘ran 𝐺) → (1...𝑚) = (1...(♯‘ran 𝐺)))
101100f1oeq2d 6471 . . . . . . . . . 10 (𝑚 = (♯‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran 𝐺𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
102101exbidv 1897 . . . . . . . . 9 (𝑚 = (♯‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺 ↔ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
103102rspcev 3554 . . . . . . . 8 (((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
10499, 103syl 17 . . . . . . 7 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
105 r19.29 3215 . . . . . . 7 ((∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
10669, 104, 105syl2anc 584 . . . . . 6 (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
107 exdistrv 1931 . . . . . . . . 9 (∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
108107biimpri 229 . . . . . . . 8 ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
109108a1i 11 . . . . . . 7 (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
110109reximdv 3233 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
111106, 110mpd 15 . . . . 5 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
112 df-rex 3109 . . . . 5 (∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
113111, 112sylib 219 . . . 4 (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
114 ax-5 1886 . . . . . . . . 9 (𝑚 ∈ ℕ → ∀𝑔 𝑚 ∈ ℕ)
115 19.29 1853 . . . . . . . . 9 ((∀𝑔 𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
116114, 115sylan 580 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
117 ax-5 1886 . . . . . . . . . 10 (𝑚 ∈ ℕ → ∀𝑓 𝑚 ∈ ℕ)
118 19.29 1853 . . . . . . . . . 10 ((∀𝑓 𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
119117, 118sylan 580 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
120119eximi 1814 . . . . . . . 8 (∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
121116, 120syl 17 . . . . . . 7 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
122 df-3an 1080 . . . . . . . . 9 ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
123122anbi2i 622 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1241232exbii 1828 . . . . . . 7 (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
125121, 124sylibr 235 . . . . . 6 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
126125a1i 11 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
127126eximdv 1893 . . . 4 (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
128113, 127mpd 15 . . 3 (𝜑 → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
12982adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑄 ∈ V)
130 simprl 767 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑚 ∈ ℕ)
131 simprr1 1212 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑔 Fn ran 𝐺)
132 elex 3450 . . . . . . . . 9 (ran 𝐺 ∈ Fin → ran 𝐺 ∈ V)
1334, 132syl 17 . . . . . . . 8 (𝜑 → ran 𝐺 ∈ V)
134133adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ran 𝐺 ∈ V)
135 simprr2 1213 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
13651rspccva 3553 . . . . . . . 8 ((∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
137135, 136sylan 580 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
138 simprr3 1214 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
13970adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → (𝑇𝑈) ⊆ 𝑋)
140 stoweidlem35.1 . . . . . . . 8 𝑡𝜑
141 nfv 1890 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
142 nfcv 2947 . . . . . . . . . . 11 𝑡𝑔
143 nfcv 2947 . . . . . . . . . . . . . 14 𝑡𝑋
144 nfrab1 3341 . . . . . . . . . . . . . . . 16 𝑡{𝑡𝑇 ∣ 0 < (𝑡)}
145144nfeq2 2962 . . . . . . . . . . . . . . 15 𝑡 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}
146 nfv 1890 . . . . . . . . . . . . . . . . . 18 𝑡(𝑍) = 0
147 nfra1 3184 . . . . . . . . . . . . . . . . . 18 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
148146, 147nfan 1879 . . . . . . . . . . . . . . . . 17 𝑡((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))
149 nfcv 2947 . . . . . . . . . . . . . . . . 17 𝑡𝐴
150148, 149nfrab 3342 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
15180, 150nfcxfr 2945 . . . . . . . . . . . . . . 15 𝑡𝑄
152145, 151nfrab 3342 . . . . . . . . . . . . . 14 𝑡{𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
153143, 152nfmpt 5051 . . . . . . . . . . . . 13 𝑡(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
1542, 153nfcxfr 2945 . . . . . . . . . . . 12 𝑡𝐺
155154nfrn 5698 . . . . . . . . . . 11 𝑡ran 𝐺
156142, 155nffn 6314 . . . . . . . . . 10 𝑡 𝑔 Fn ran 𝐺
157 nfv 1890 . . . . . . . . . . 11 𝑡(𝑔𝑙) ∈ 𝑙
158155, 157nfral 3189 . . . . . . . . . 10 𝑡𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
159 nfcv 2947 . . . . . . . . . . 11 𝑡𝑓
160 nfcv 2947 . . . . . . . . . . 11 𝑡(1...𝑚)
161159, 160, 155nff1o 6473 . . . . . . . . . 10 𝑡 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
162156, 158, 161nf3an 1881 . . . . . . . . 9 𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
163141, 162nfan 1879 . . . . . . . 8 𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
164140, 163nfan 1879 . . . . . . 7 𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
165 nfv 1890 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
166 nfcv 2947 . . . . . . . . . . 11 𝑤𝑔
167166, 11nffn 6314 . . . . . . . . . 10 𝑤 𝑔 Fn ran 𝐺
168 nfv 1890 . . . . . . . . . . 11 𝑤(𝑔𝑙) ∈ 𝑙
16911, 168nfral 3189 . . . . . . . . . 10 𝑤𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
170 nfcv 2947 . . . . . . . . . . 11 𝑤𝑓
171 nfcv 2947 . . . . . . . . . . 11 𝑤(1...𝑚)
172170, 171, 11nff1o 6473 . . . . . . . . . 10 𝑤 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
173167, 169, 172nf3an 1881 . . . . . . . . 9 𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
174165, 173nfan 1879 . . . . . . . 8 𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
1758, 174nfan 1879 . . . . . . 7 𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1762, 129, 130, 131, 134, 137, 138, 139, 164, 175, 84stoweidlem27 41808 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
177176ex 413 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
1781772eximdv 1895 . . . 4 (𝜑 → (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
179178eximdv 1893 . . 3 (𝜑 → (∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
180128, 179mpd 15 . 2 (𝜑 → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
181 id 22 . . . 4 (∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
182181exlimivv 1908 . . 3 (∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
183182eximi 1814 . 2 (∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
184180, 183syl 17 1 (𝜑 → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 842  w3a 1078  wal 1518   = wceq 1520  wex 1759  wnf 1763  wcel 2079  wne 2982  wral 3103  wrex 3104  {crab 3107  Vcvv 3432  cdif 3851  wss 3854  c0 4206   cuni 4739   class class class wbr 4956  cmpt 5035  dom cdm 5435  ran crn 5436   Fn wfn 6212  wf 6213  1-1-ontowf1o 6216  cfv 6217  (class class class)co 7007  Fincfn 8347  0cc0 10372  1c1 10373   < clt 10510  cle 10511  cn 11475  ...cfz 12731  chash 13528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-rep 5075  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429  ax-1cn 10430  ax-icn 10431  ax-addcl 10432  ax-addrcl 10433  ax-mulcl 10434  ax-mulrcl 10435  ax-mulcom 10436  ax-addass 10437  ax-mulass 10438  ax-distr 10439  ax-i2m1 10440  ax-1ne0 10441  ax-1rid 10442  ax-rnegex 10443  ax-rrecex 10444  ax-cnre 10445  ax-pre-lttri 10446  ax-pre-lttrn 10447  ax-pre-ltadd 10448  ax-pre-mulgt0 10449
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-nel 3089  df-ral 3108  df-rex 3109  df-reu 3110  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-pss 3871  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-tp 4471  df-op 4473  df-uni 4740  df-int 4777  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-tr 5058  df-id 5340  df-eprel 5345  df-po 5354  df-so 5355  df-fr 5394  df-we 5396  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-pred 6015  df-ord 6061  df-on 6062  df-lim 6063  df-suc 6064  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-f1 6222  df-fo 6223  df-f1o 6224  df-fv 6225  df-riota 6968  df-ov 7010  df-oprab 7011  df-mpo 7012  df-om 7428  df-1st 7536  df-2nd 7537  df-wrecs 7789  df-recs 7851  df-rdg 7889  df-1o 7944  df-oadd 7948  df-er 8130  df-en 8348  df-dom 8349  df-sdom 8350  df-fin 8351  df-card 9203  df-pnf 10512  df-mnf 10513  df-xr 10514  df-ltxr 10515  df-le 10516  df-sub 10708  df-neg 10709  df-nn 11476  df-n0 11735  df-z 11819  df-uz 12083  df-fz 12732  df-hash 13529
This theorem is referenced by:  stoweidlem53  41834
  Copyright terms: Public domain W3C validator