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 38728
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 38145 . . . . . . . . . 10 (𝑋 ∈ Fin → ran 𝐺 ∈ Fin)
41, 3syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
5 fnchoice 38010 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
65adantl 480 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
7 simprl 789 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺)
8 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝜑
9 nfmpt1 4665 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
102, 9nfcxfr 2744 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤𝐺
1110nfrn 5272 . . . . . . . . . . . . . . . . . . . . . 22 𝑤ran 𝐺
1211nfcri 2740 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑘 ∈ ran 𝐺
138, 12nfan 1814 . . . . . . . . . . . . . . . . . . . 20 𝑤(𝜑𝑘 ∈ ran 𝐺)
14 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋𝑊)
1514sselda 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑋) → 𝑤𝑊)
16 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
1715, 16syl6eleq 2693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑋) → 𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
18 rabid 3090 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
1917, 18sylib 206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑋) → (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2019simprd 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑋) → ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)})
21 df-rex 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2220, 21sylib 206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑋) → ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
23 rabid 3090 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2423exbii 1762 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2522, 24sylibr 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2625adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
27 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝜑
28 nfv 1828 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝑋
2927, 28nfan 1814 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑤𝑋)
30 nfrab1 3094 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3130nfeq2 2761 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3229, 31nfan 1814 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 eleq2 2672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → (𝑘 ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
3433biimprd 236 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3534adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3632, 35eximd 2069 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ∃ 𝑘))
3726, 36mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
3837adantllr 750 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
392elrnmpt 5276 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4039ibi 254 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ran 𝐺 → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4140adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ran 𝐺) → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4213, 38, 41r19.29af 3053 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ran 𝐺) → ∃ 𝑘)
43 n0 3885 . . . . . . . . . . . . . . . . . . 19 (𝑘 ≠ ∅ ↔ ∃ 𝑘)
4442, 43sylibr 222 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
4544adantlr 746 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
46 simplrr 796 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))
47 neeq1 2839 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅))
48 fveq2 6084 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑘 → (𝑔𝑙) = (𝑔𝑘))
4948eleq1d 2667 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑙))
50 eleq2 2672 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑘) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5149, 50bitrd 266 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5247, 51imbi12d 332 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘)))
5352rspccva 3276 . . . . . . . . . . . . . . . . . 18 ((∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5446, 53sylancom 697 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5545, 54mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
5655ralrimiva 2944 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘)
57 fveq2 6084 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑔𝑘) = (𝑔𝑙))
5857eleq1d 2667 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑘))
59 eleq2 2672 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑙) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6058, 59bitrd 266 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6160cbvralv 3142 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
6256, 61sylib 206 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
637, 62jca 552 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6463ex 448 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6564adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6665eximdv 1831 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
676, 66mpd 15 . . . . . . . . 9 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
684, 67mpdan 698 . . . . . . . 8 (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6968ralrimivw 2945 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
70 stoweidlem35.10 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
71 stoweidlem35.11 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ≠ ∅)
72 ssn0 3923 . . . . . . . . . . . . 13 (((𝑇𝑈) ⊆ 𝑋 ∧ (𝑇𝑈) ≠ ∅) → 𝑋 ≠ ∅)
7370, 71, 72syl2anc 690 . . . . . . . . . . . 12 (𝜑 𝑋 ≠ ∅)
7473neneqd 2782 . . . . . . . . . . 11 (𝜑 → ¬ 𝑋 = ∅)
75 unieq 4370 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑋 = ∅)
76 uni0 4391 . . . . . . . . . . . 12 ∅ = ∅
7775, 76syl6eq 2655 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑋 = ∅)
7874, 77nsyl 133 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
79 dm0rn0 5246 . . . . . . . . . . 11 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
80 stoweidlem35.4 . . . . . . . . . . . . . . . . . 18 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
81 stoweidlem35.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
8280, 81rabexd 4732 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ V)
83 nfrab1 3094 . . . . . . . . . . . . . . . . . . 19 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
8480, 83nfcxfr 2744 . . . . . . . . . . . . . . . . . 18 𝑄
8584rabexgf 38005 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8682, 85syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8786adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
888, 87, 2fmptdf 6275 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋⟶V)
89 dffn2 5942 . . . . . . . . . . . . . 14 (𝐺 Fn 𝑋𝐺:𝑋⟶V)
9088, 89sylibr 222 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
91 fndm 5886 . . . . . . . . . . . . 13 (𝐺 Fn 𝑋 → dom 𝐺 = 𝑋)
9290, 91syl 17 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝑋)
9392eqeq1d 2607 . . . . . . . . . . 11 (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅))
9479, 93syl5bbr 272 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅))
9578, 94mtbird 313 . . . . . . . . 9 (𝜑 → ¬ ran 𝐺 = ∅)
96 fz1f1o 14230 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
974, 96syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ∨ ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9897ord 390 . . . . . . . . 9 (𝜑 → (¬ ran 𝐺 = ∅ → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺)))
9995, 98mpd 15 . . . . . . . 8 (𝜑 → ((#‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
100 oveq2 6531 . . . . . . . . . . 11 (𝑚 = (#‘ran 𝐺) → (1...𝑚) = (1...(#‘ran 𝐺)))
101 f1oeq2 6022 . . . . . . . . . . 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 1835 . . . . . . . . 9 (𝑚 = (#‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺 ↔ ∃𝑓 𝑓:(1...(#‘ran 𝐺))–1-1-onto→ran 𝐺))
104103rspcev 3277 . . . . . . . 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 3049 . . . . . . 7 ((∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
10769, 105, 106syl2anc 690 . . . . . 6 (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
108 eeanv 2164 . . . . . . . . 9 (∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
109108biimpri 216 . . . . . . . 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 2994 . . . . . 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 2897 . . . . 5 (∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
114112, 113sylib 206 . . . 4 (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
115 ax-5 1825 . . . . . . . . 9 (𝑚 ∈ ℕ → ∀𝑔 𝑚 ∈ ℕ)
116 19.29 1787 . . . . . . . . 9 ((∀𝑔 𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
117115, 116sylan 486 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
118 ax-5 1825 . . . . . . . . . 10 (𝑚 ∈ ℕ → ∀𝑓 𝑚 ∈ ℕ)
119 19.29 1787 . . . . . . . . . 10 ((∀𝑓 𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
120118, 119sylan 486 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
121120eximi 1750 . . . . . . . 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 1032 . . . . . . . . 9 ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
124123anbi2i 725 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1251242exbii 1763 . . . . . . 7 (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
126122, 125sylibr 222 . . . . . 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 1831 . . . 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 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑄 ∈ V)
131 simprl 789 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑚 ∈ ℕ)
132 simprr1 1101 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑔 Fn ran 𝐺)
133 elex 3180 . . . . . . . . 9 (ran 𝐺 ∈ Fin → ran 𝐺 ∈ V)
1344, 133syl 17 . . . . . . . 8 (𝜑 → ran 𝐺 ∈ V)
135134adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ran 𝐺 ∈ V)
136 simprr2 1102 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
13751rspccva 3276 . . . . . . . 8 ((∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
138136, 137sylan 486 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
139 simprr3 1103 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
14070adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → (𝑇𝑈) ⊆ 𝑋)
141 stoweidlem35.1 . . . . . . . 8 𝑡𝜑
142 nfv 1828 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
143 nfcv 2746 . . . . . . . . . . 11 𝑡𝑔
144 nfcv 2746 . . . . . . . . . . . . . 14 𝑡𝑋
145 nfrab1 3094 . . . . . . . . . . . . . . . 16 𝑡{𝑡𝑇 ∣ 0 < (𝑡)}
146145nfeq2 2761 . . . . . . . . . . . . . . 15 𝑡 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}
147 nfv 1828 . . . . . . . . . . . . . . . . . 18 𝑡(𝑍) = 0
148 nfra1 2920 . . . . . . . . . . . . . . . . . 18 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
149147, 148nfan 1814 . . . . . . . . . . . . . . . . 17 𝑡((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))
150 nfcv 2746 . . . . . . . . . . . . . . . . 17 𝑡𝐴
151149, 150nfrab 3095 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
15280, 151nfcxfr 2744 . . . . . . . . . . . . . . 15 𝑡𝑄
153146, 152nfrab 3095 . . . . . . . . . . . . . 14 𝑡{𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
154144, 153nfmpt 4664 . . . . . . . . . . . . 13 𝑡(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
1552, 154nfcxfr 2744 . . . . . . . . . . . 12 𝑡𝐺
156155nfrn 5272 . . . . . . . . . . 11 𝑡ran 𝐺
157143, 156nffn 5883 . . . . . . . . . 10 𝑡 𝑔 Fn ran 𝐺
158 nfv 1828 . . . . . . . . . . 11 𝑡(𝑔𝑙) ∈ 𝑙
159156, 158nfral 2924 . . . . . . . . . 10 𝑡𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
160 nfcv 2746 . . . . . . . . . . 11 𝑡𝑓
161 nfcv 2746 . . . . . . . . . . 11 𝑡(1...𝑚)
162160, 161, 156nff1o 6029 . . . . . . . . . 10 𝑡 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
163157, 159, 162nf3an 1817 . . . . . . . . 9 𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
164142, 163nfan 1814 . . . . . . . 8 𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
165141, 164nfan 1814 . . . . . . 7 𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
166 nfv 1828 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
167 nfcv 2746 . . . . . . . . . . 11 𝑤𝑔
168167, 11nffn 5883 . . . . . . . . . 10 𝑤 𝑔 Fn ran 𝐺
169 nfv 1828 . . . . . . . . . . 11 𝑤(𝑔𝑙) ∈ 𝑙
17011, 169nfral 2924 . . . . . . . . . 10 𝑤𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
171 nfcv 2746 . . . . . . . . . . 11 𝑤𝑓
172 nfcv 2746 . . . . . . . . . . 11 𝑤(1...𝑚)
173171, 172, 11nff1o 6029 . . . . . . . . . 10 𝑤 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
174168, 170, 173nf3an 1817 . . . . . . . . 9 𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
175166, 174nfan 1814 . . . . . . . 8 𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
1768, 175nfan 1814 . . . . . . 7 𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1772, 130, 131, 132, 135, 138, 139, 140, 165, 176, 84stoweidlem27 38720 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
178177ex 448 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
1791782eximdv 1833 . . . 4 (𝜑 → (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
180179eximdv 1831 . . 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 1845 . . 3 (∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
184183eximi 1750 . 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 194  wo 381  wa 382  w3a 1030  wal 1472   = wceq 1474  wex 1694  wnf 1698  wcel 1975  wne 2775  wral 2891  wrex 2892  {crab 2895  Vcvv 3168  cdif 3532  wss 3535  c0 3869   cuni 4362   class class class wbr 4573  cmpt 4633  dom cdm 5024  ran crn 5025   Fn wfn 5781  wf 5782  1-1-ontowf1o 5785  cfv 5786  (class class class)co 6523  Fincfn 7814  0cc0 9788  1c1 9789   < clt 9926  cle 9927  cn 10863  ...cfz 12148  #chash 12930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-rep 4689  ax-sep 4699  ax-nul 4708  ax-pow 4760  ax-pr 4824  ax-un 6820  ax-cnex 9844  ax-resscn 9845  ax-1cn 9846  ax-icn 9847  ax-addcl 9848  ax-addrcl 9849  ax-mulcl 9850  ax-mulrcl 9851  ax-mulcom 9852  ax-addass 9853  ax-mulass 9854  ax-distr 9855  ax-i2m1 9856  ax-1ne0 9857  ax-1rid 9858  ax-rnegex 9859  ax-rrecex 9860  ax-cnre 9861  ax-pre-lttri 9862  ax-pre-lttrn 9863  ax-pre-ltadd 9864  ax-pre-mulgt0 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ne 2777  df-nel 2778  df-ral 2896  df-rex 2897  df-reu 2898  df-rab 2900  df-v 3170  df-sbc 3398  df-csb 3495  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-pss 3551  df-nul 3870  df-if 4032  df-pw 4105  df-sn 4121  df-pr 4123  df-tp 4125  df-op 4127  df-uni 4363  df-int 4401  df-iun 4447  df-br 4574  df-opab 4634  df-mpt 4635  df-tr 4671  df-eprel 4935  df-id 4939  df-po 4945  df-so 4946  df-fr 4983  df-we 4985  df-xp 5030  df-rel 5031  df-cnv 5032  df-co 5033  df-dm 5034  df-rn 5035  df-res 5036  df-ima 5037  df-pred 5579  df-ord 5625  df-on 5626  df-lim 5627  df-suc 5628  df-iota 5750  df-fun 5788  df-fn 5789  df-f 5790  df-f1 5791  df-fo 5792  df-f1o 5793  df-fv 5794  df-riota 6485  df-ov 6526  df-oprab 6527  df-mpt2 6528  df-om 6931  df-1st 7032  df-2nd 7033  df-wrecs 7267  df-recs 7328  df-rdg 7366  df-1o 7420  df-oadd 7424  df-er 7602  df-en 7815  df-dom 7816  df-sdom 7817  df-fin 7818  df-card 8621  df-pnf 9928  df-mnf 9929  df-xr 9930  df-ltxr 9931  df-le 9932  df-sub 10115  df-neg 10116  df-nn 10864  df-n0 11136  df-z 11207  df-uz 11516  df-fz 12149  df-hash 12931
This theorem is referenced by:  stoweidlem53  38746
  Copyright terms: Public domain W3C validator