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 40570
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 39665 . . . . . . . . . 10 (𝑋 ∈ Fin → ran 𝐺 ∈ Fin)
41, 3syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
5 fnchoice 39502 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
65adantl 481 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
7 simprl 809 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺)
8 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝜑
9 nfmpt1 4780 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
102, 9nfcxfr 2791 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤𝐺
1110nfrn 5400 . . . . . . . . . . . . . . . . . . . . . 22 𝑤ran 𝐺
1211nfcri 2787 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑘 ∈ ran 𝐺
138, 12nfan 1868 . . . . . . . . . . . . . . . . . . . 20 𝑤(𝜑𝑘 ∈ ran 𝐺)
14 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋𝑊)
1514sselda 3636 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑋) → 𝑤𝑊)
16 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
1715, 16syl6eleq 2740 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑋) → 𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
18 rabid 3145 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
1917, 18sylib 208 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑋) → (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2019simprd 478 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑋) → ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)})
21 df-rex 2947 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2220, 21sylib 208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑋) → ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
23 rabid 3145 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2423exbii 1814 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2522, 24sylibr 224 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2625adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
27 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝜑
28 nfv 1883 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝑋
2927, 28nfan 1868 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑤𝑋)
30 nfrab1 3152 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3130nfeq2 2809 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3229, 31nfan 1868 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → (𝑘 ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
3433biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3534adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3632, 35eximd 2123 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ∃ 𝑘))
3726, 36mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
3837adantllr 755 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
392elrnmpt 5404 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4039ibi 256 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ran 𝐺 → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4140adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ran 𝐺) → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4213, 38, 41r19.29af 3105 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ran 𝐺) → ∃ 𝑘)
43 n0 3964 . . . . . . . . . . . . . . . . . . 19 (𝑘 ≠ ∅ ↔ ∃ 𝑘)
4442, 43sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
4544adantlr 751 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
46 simplrr 818 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))
47 neeq1 2885 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅))
48 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑘 → (𝑔𝑙) = (𝑔𝑘))
4948eleq1d 2715 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑙))
50 eleq2 2719 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑘) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5149, 50bitrd 268 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5247, 51imbi12d 333 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘)))
5352rspccva 3339 . . . . . . . . . . . . . . . . . 18 ((∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5446, 53sylancom 702 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5545, 54mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
5655ralrimiva 2995 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘)
57 fveq2 6229 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑔𝑘) = (𝑔𝑙))
5857eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑘))
59 eleq2 2719 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑙) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6058, 59bitrd 268 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6160cbvralv 3201 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
6256, 61sylib 208 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
637, 62jca 553 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6463ex 449 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6564adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6665eximdv 1886 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
676, 66mpd 15 . . . . . . . . 9 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
684, 67mpdan 703 . . . . . . . 8 (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6968ralrimivw 2996 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
70 stoweidlem35.10 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
71 stoweidlem35.11 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ≠ ∅)
72 ssn0 4009 . . . . . . . . . . . . 13 (((𝑇𝑈) ⊆ 𝑋 ∧ (𝑇𝑈) ≠ ∅) → 𝑋 ≠ ∅)
7370, 71, 72syl2anc 694 . . . . . . . . . . . 12 (𝜑 𝑋 ≠ ∅)
7473neneqd 2828 . . . . . . . . . . 11 (𝜑 → ¬ 𝑋 = ∅)
75 unieq 4476 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑋 = ∅)
76 uni0 4497 . . . . . . . . . . . 12 ∅ = ∅
7775, 76syl6eq 2701 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑋 = ∅)
7874, 77nsyl 135 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
79 dm0rn0 5374 . . . . . . . . . . 11 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
80 stoweidlem35.4 . . . . . . . . . . . . . . . . . 18 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
81 stoweidlem35.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
8280, 81rabexd 4846 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ V)
83 nfrab1 3152 . . . . . . . . . . . . . . . . . . 19 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
8480, 83nfcxfr 2791 . . . . . . . . . . . . . . . . . 18 𝑄
8584rabexgf 39497 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8682, 85syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8786adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
888, 87, 2fmptdf 6427 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋⟶V)
89 dffn2 6085 . . . . . . . . . . . . . 14 (𝐺 Fn 𝑋𝐺:𝑋⟶V)
9088, 89sylibr 224 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
91 fndm 6028 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋)
9290, 91syl 17 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝑋)
9392eqeq1d 2653 . . . . . . . . . . 11 (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅))
9479, 93syl5bbr 274 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅))
9578, 94mtbird 314 . . . . . . . . 9 (𝜑 → ¬ ran 𝐺 = ∅)
96 fz1f1o 14485 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
974, 96syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9897ord 391 . . . . . . . . 9 (𝜑 → (¬ ran 𝐺 = ∅ → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9995, 98mpd 15 . . . . . . . 8 (𝜑 → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
100 oveq2 6698 . . . . . . . . . . 11 (𝑚 = (#‘ran 𝐺) → (1...𝑚) = (1...(#‘ran 𝐺)))
101 f1oeq2 6166 . . . . . . . . . . 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 1890 . . . . . . . . 9 (𝑚 = (#‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺 ↔ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
104103rspcev 3340 . . . . . . . 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 3101 . . . . . . 7 ((∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
10769, 105, 106syl2anc 694 . . . . . 6 (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
108 eeanv 2218 . . . . . . . . 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 3045 . . . . . 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 2947 . . . . 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 1879 . . . . . . . . 9 (𝑚 ∈ ℕ → ∀𝑔 𝑚 ∈ ℕ)
116 19.29 1841 . . . . . . . . 9 ((∀𝑔 𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
117115, 116sylan 487 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
118 ax-5 1879 . . . . . . . . . 10 (𝑚 ∈ ℕ → ∀𝑓 𝑚 ∈ ℕ)
119 19.29 1841 . . . . . . . . . 10 ((∀𝑓 𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
120118, 119sylan 487 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
121120eximi 1802 . . . . . . . 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 1056 . . . . . . . . 9 ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
124123anbi2i 730 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1251242exbii 1815 . . . . . . 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 1886 . . . 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 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑄 ∈ V)
131 simprl 809 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑚 ∈ ℕ)
132 simprr1 1129 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑔 Fn ran 𝐺)
133 elex 3243 . . . . . . . . 9 (ran 𝐺 ∈ Fin → ran 𝐺 ∈ V)
1344, 133syl 17 . . . . . . . 8 (𝜑 → ran 𝐺 ∈ V)
135134adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ran 𝐺 ∈ V)
136 simprr2 1130 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
13751rspccva 3339 . . . . . . . 8 ((∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
138136, 137sylan 487 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
139 simprr3 1131 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
14070adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → (𝑇𝑈) ⊆ 𝑋)
141 stoweidlem35.1 . . . . . . . 8 𝑡𝜑
142 nfv 1883 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
143 nfcv 2793 . . . . . . . . . . 11 𝑡𝑔
144 nfcv 2793 . . . . . . . . . . . . . 14 𝑡𝑋
145 nfrab1 3152 . . . . . . . . . . . . . . . 16 𝑡{𝑡𝑇 ∣ 0 < (𝑡)}
146145nfeq2 2809 . . . . . . . . . . . . . . 15 𝑡 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}
147 nfv 1883 . . . . . . . . . . . . . . . . . 18 𝑡(𝑍) = 0
148 nfra1 2970 . . . . . . . . . . . . . . . . . 18 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
149147, 148nfan 1868 . . . . . . . . . . . . . . . . 17 𝑡((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))
150 nfcv 2793 . . . . . . . . . . . . . . . . 17 𝑡𝐴
151149, 150nfrab 3153 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
15280, 151nfcxfr 2791 . . . . . . . . . . . . . . 15 𝑡𝑄
153146, 152nfrab 3153 . . . . . . . . . . . . . 14 𝑡{𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
154144, 153nfmpt 4779 . . . . . . . . . . . . 13 𝑡(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
1552, 154nfcxfr 2791 . . . . . . . . . . . 12 𝑡𝐺
156155nfrn 5400 . . . . . . . . . . 11 𝑡ran 𝐺
157143, 156nffn 6025 . . . . . . . . . 10 𝑡 𝑔 Fn ran 𝐺
158 nfv 1883 . . . . . . . . . . 11 𝑡(𝑔𝑙) ∈ 𝑙
159156, 158nfral 2974 . . . . . . . . . 10 𝑡𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
160 nfcv 2793 . . . . . . . . . . 11 𝑡𝑓
161 nfcv 2793 . . . . . . . . . . 11 𝑡(1...𝑚)
162160, 161, 156nff1o 6173 . . . . . . . . . 10 𝑡 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
163157, 159, 162nf3an 1871 . . . . . . . . 9 𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
164142, 163nfan 1868 . . . . . . . 8 𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
165141, 164nfan 1868 . . . . . . 7 𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
166 nfv 1883 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
167 nfcv 2793 . . . . . . . . . . 11 𝑤𝑔
168167, 11nffn 6025 . . . . . . . . . 10 𝑤 𝑔 Fn ran 𝐺
169 nfv 1883 . . . . . . . . . . 11 𝑤(𝑔𝑙) ∈ 𝑙
17011, 169nfral 2974 . . . . . . . . . 10 𝑤𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
171 nfcv 2793 . . . . . . . . . . 11 𝑤𝑓
172 nfcv 2793 . . . . . . . . . . 11 𝑤(1...𝑚)
173171, 172, 11nff1o 6173 . . . . . . . . . 10 𝑤 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
174168, 170, 173nf3an 1871 . . . . . . . . 9 𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
175166, 174nfan 1868 . . . . . . . 8 𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
1768, 175nfan 1868 . . . . . . 7 𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1772, 130, 131, 132, 135, 138, 139, 140, 165, 176, 84stoweidlem27 40562 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
178177ex 449 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
1791782eximdv 1888 . . . 4 (𝜑 → (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
180179eximdv 1886 . . 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 1900 . . 3 (∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
184183eximi 1802 . 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 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wex 1744  wnf 1748  wcel 2030  wne 2823  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  cdif 3604  wss 3607  c0 3948   cuni 4468   class class class wbr 4685  cmpt 4762  dom cdm 5143  ran crn 5144   Fn wfn 5921  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Fincfn 7997  0cc0 9974  1c1 9975   < clt 10112  cle 10113  cn 11058  ...cfz 12364  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158
This theorem is referenced by:  stoweidlem53  40588
  Copyright terms: Public domain W3C validator