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 45656
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 44778 . . . . . . . . . 10 (𝑋 ∈ Fin → ran 𝐺 ∈ Fin)
41, 3syl 17 . . . . . . . . 9 (𝜑 → ran 𝐺 ∈ Fin)
5 fnchoice 44628 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
65adantl 480 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)))
7 simprl 769 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → 𝑔 Fn ran 𝐺)
8 stoweidlem35.2 . . . . . . . . . . . . . . . . . . . . 21 𝑤𝜑
9 nfmpt1 5261 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑤(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
102, 9nfcxfr 2890 . . . . . . . . . . . . . . . . . . . . . . 23 𝑤𝐺
1110nfrn 5958 . . . . . . . . . . . . . . . . . . . . . 22 𝑤ran 𝐺
1211nfcri 2883 . . . . . . . . . . . . . . . . . . . . 21 𝑤 𝑘 ∈ ran 𝐺
138, 12nfan 1895 . . . . . . . . . . . . . . . . . . . 20 𝑤(𝜑𝑘 ∈ ran 𝐺)
14 stoweidlem35.9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑𝑋𝑊)
1514sselda 3979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝜑𝑤𝑋) → 𝑤𝑊)
16 stoweidlem35.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑊 = {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
1715, 16eleqtrdi 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑤𝑋) → 𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
18 rabid 3440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑤 ∈ {𝑤𝐽 ∣ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
1917, 18sylib 217 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑𝑤𝑋) → (𝑤𝐽 ∧ ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2019simprd 494 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑𝑤𝑋) → ∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)})
21 df-rex 3061 . . . . . . . . . . . . . . . . . . . . . . . . 25 (∃𝑄 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2220, 21sylib 217 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑤𝑋) → ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
23 rabid 3440 . . . . . . . . . . . . . . . . . . . . . . . . 25 ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ (𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2423exbii 1843 . . . . . . . . . . . . . . . . . . . . . . . 24 (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ↔ ∃(𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}))
2522, 24sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
2625adantr 479 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
27 stoweidlem35.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝜑
28 nfv 1910 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑤𝑋
2927, 28nfan 1895 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑤𝑋)
30 nfrab1 3439 . . . . . . . . . . . . . . . . . . . . . . . . 25 {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3130nfeq2 2910 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
3229, 31nfan 1895 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
33 eleq2 2815 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → (𝑘 ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
3433biimprd 247 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3534adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ( ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → 𝑘))
3632, 35eximd 2205 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → (∃ ∈ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} → ∃ 𝑘))
3726, 36mpd 15 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
3837adantllr 717 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑘 ∈ ran 𝐺) ∧ 𝑤𝑋) ∧ 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}) → ∃ 𝑘)
392elrnmpt 5962 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘 ∈ ran 𝐺 → (𝑘 ∈ ran 𝐺 ↔ ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}))
4039ibi 266 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ∈ ran 𝐺 → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4140adantl 480 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ ran 𝐺) → ∃𝑤𝑋 𝑘 = {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
4213, 38, 41r19.29af 3256 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ ran 𝐺) → ∃ 𝑘)
43 n0 4349 . . . . . . . . . . . . . . . . . . 19 (𝑘 ≠ ∅ ↔ ∃ 𝑘)
4442, 43sylibr 233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
4544adantlr 713 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → 𝑘 ≠ ∅)
46 simplrr 776 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))
47 neeq1 2993 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → (𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅))
48 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . 22 (𝑙 = 𝑘 → (𝑔𝑙) = (𝑔𝑘))
4948eleq1d 2811 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑙))
50 eleq2 2815 . . . . . . . . . . . . . . . . . . . . 21 (𝑙 = 𝑘 → ((𝑔𝑘) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5149, 50bitrd 278 . . . . . . . . . . . . . . . . . . . 20 (𝑙 = 𝑘 → ((𝑔𝑙) ∈ 𝑙 ↔ (𝑔𝑘) ∈ 𝑘))
5247, 51imbi12d 343 . . . . . . . . . . . . . . . . . . 19 (𝑙 = 𝑘 → ((𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ↔ (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘)))
5352rspccva 3607 . . . . . . . . . . . . . . . . . 18 ((∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5446, 53sylancom 586 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑘 ≠ ∅ → (𝑔𝑘) ∈ 𝑘))
5545, 54mpd 15 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
5655ralrimiva 3136 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘)
57 fveq2 6901 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑙 → (𝑔𝑘) = (𝑔𝑙))
5857eleq1d 2811 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑘))
59 eleq2 2815 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑙 → ((𝑔𝑙) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6058, 59bitrd 278 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑙 → ((𝑔𝑘) ∈ 𝑘 ↔ (𝑔𝑙) ∈ 𝑙))
6160cbvralvw 3225 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ran 𝐺(𝑔𝑘) ∈ 𝑘 ↔ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
6256, 61sylib 217 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
637, 62jca 510 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙))) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6463ex 411 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6564adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
6665eximdv 1913 . . . . . . . . . 10 ((𝜑 ∧ ran 𝐺 ∈ Fin) → (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑙 ≠ ∅ → (𝑔𝑙) ∈ 𝑙)) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)))
676, 66mpd 15 . . . . . . . . 9 ((𝜑 ∧ ran 𝐺 ∈ Fin) → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
684, 67mpdan 685 . . . . . . . 8 (𝜑 → ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
6968ralrimivw 3140 . . . . . . 7 (𝜑 → ∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙))
70 stoweidlem35.10 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ⊆ 𝑋)
71 stoweidlem35.11 . . . . . . . . . . . . 13 (𝜑 → (𝑇𝑈) ≠ ∅)
72 ssn0 4405 . . . . . . . . . . . . 13 (((𝑇𝑈) ⊆ 𝑋 ∧ (𝑇𝑈) ≠ ∅) → 𝑋 ≠ ∅)
7370, 71, 72syl2anc 582 . . . . . . . . . . . 12 (𝜑 𝑋 ≠ ∅)
7473neneqd 2935 . . . . . . . . . . 11 (𝜑 → ¬ 𝑋 = ∅)
75 unieq 4924 . . . . . . . . . . . 12 (𝑋 = ∅ → 𝑋 = ∅)
76 uni0 4943 . . . . . . . . . . . 12 ∅ = ∅
7775, 76eqtrdi 2782 . . . . . . . . . . 11 (𝑋 = ∅ → 𝑋 = ∅)
7874, 77nsyl 140 . . . . . . . . . 10 (𝜑 → ¬ 𝑋 = ∅)
79 dm0rn0 5931 . . . . . . . . . . 11 (dom 𝐺 = ∅ ↔ ran 𝐺 = ∅)
80 stoweidlem35.4 . . . . . . . . . . . . . . . . . 18 𝑄 = {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
81 stoweidlem35.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 ∈ V)
8280, 81rabexd 5340 . . . . . . . . . . . . . . . . 17 (𝜑𝑄 ∈ V)
83 nfrab1 3439 . . . . . . . . . . . . . . . . . . 19 {𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
8480, 83nfcxfr 2890 . . . . . . . . . . . . . . . . . 18 𝑄
8584rabexgf 44623 . . . . . . . . . . . . . . . . 17 (𝑄 ∈ V → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8682, 85syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
8786adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑤𝑋) → {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}} ∈ V)
888, 87, 2fmptdf 7131 . . . . . . . . . . . . . 14 (𝜑𝐺:𝑋⟶V)
89 dffn2 6730 . . . . . . . . . . . . . 14 (𝐺 Fn 𝑋𝐺:𝑋⟶V)
9088, 89sylibr 233 . . . . . . . . . . . . 13 (𝜑𝐺 Fn 𝑋)
9190fndmd 6665 . . . . . . . . . . . 12 (𝜑 → dom 𝐺 = 𝑋)
9291eqeq1d 2728 . . . . . . . . . . 11 (𝜑 → (dom 𝐺 = ∅ ↔ 𝑋 = ∅))
9379, 92bitr3id 284 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ↔ 𝑋 = ∅))
9478, 93mtbird 324 . . . . . . . . 9 (𝜑 → ¬ ran 𝐺 = ∅)
95 fz1f1o 15714 . . . . . . . . . . 11 (ran 𝐺 ∈ Fin → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
964, 95syl 17 . . . . . . . . . 10 (𝜑 → (ran 𝐺 = ∅ ∨ ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
9796ord 862 . . . . . . . . 9 (𝜑 → (¬ ran 𝐺 = ∅ → ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺)))
9894, 97mpd 15 . . . . . . . 8 (𝜑 → ((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
99 oveq2 7432 . . . . . . . . . . 11 (𝑚 = (♯‘ran 𝐺) → (1...𝑚) = (1...(♯‘ran 𝐺)))
10099f1oeq2d 6839 . . . . . . . . . 10 (𝑚 = (♯‘ran 𝐺) → (𝑓:(1...𝑚)–1-1-onto→ran 𝐺𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
101100exbidv 1917 . . . . . . . . 9 (𝑚 = (♯‘ran 𝐺) → (∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺 ↔ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺))
102101rspcev 3608 . . . . . . . 8 (((♯‘ran 𝐺) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘ran 𝐺))–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
10398, 102syl 17 . . . . . . 7 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
104 r19.29 3104 . . . . . . 7 ((∀𝑚 ∈ ℕ ∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑚 ∈ ℕ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
10569, 103, 104syl2anc 582 . . . . . 6 (𝜑 → ∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
106 exdistrv 1952 . . . . . . . . 9 (∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
107106biimpri 227 . . . . . . . 8 ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
108107a1i 11 . . . . . . 7 (𝜑 → ((∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
109108reximdv 3160 . . . . . 6 (𝜑 → (∃𝑚 ∈ ℕ (∃𝑔(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ ∃𝑓 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
110105, 109mpd 15 . . . . 5 (𝜑 → ∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
111 df-rex 3061 . . . . 5 (∃𝑚 ∈ ℕ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
112110, 111sylib 217 . . . 4 (𝜑 → ∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
113 ax-5 1906 . . . . . . . . 9 (𝑚 ∈ ℕ → ∀𝑔 𝑚 ∈ ℕ)
114 19.29 1869 . . . . . . . . 9 ((∀𝑔 𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
115113, 114sylan 578 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
116 ax-5 1906 . . . . . . . . . 10 (𝑚 ∈ ℕ → ∀𝑓 𝑚 ∈ ℕ)
117 19.29 1869 . . . . . . . . . 10 ((∀𝑓 𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
118116, 117sylan 578 . . . . . . . . 9 ((𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
119118eximi 1830 . . . . . . . 8 (∃𝑔(𝑚 ∈ ℕ ∧ ∃𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
120115, 119syl 17 . . . . . . 7 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
121 df-3an 1086 . . . . . . . . 9 ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺) ↔ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
122121anbi2i 621 . . . . . . . 8 ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ (𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1231222exbii 1844 . . . . . . 7 (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) ↔ ∃𝑔𝑓(𝑚 ∈ ℕ ∧ ((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
124120, 123sylibr 233 . . . . . 6 ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
125124a1i 11 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
126125eximdv 1913 . . . 4 (𝜑 → (∃𝑚(𝑚 ∈ ℕ ∧ ∃𝑔𝑓((𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙) ∧ 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))))
127112, 126mpd 15 . . 3 (𝜑 → ∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
12882adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑄 ∈ V)
129 simprl 769 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑚 ∈ ℕ)
130 simprr1 1218 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑔 Fn ran 𝐺)
131 elex 3482 . . . . . . . . 9 (ran 𝐺 ∈ Fin → ran 𝐺 ∈ V)
1324, 131syl 17 . . . . . . . 8 (𝜑 → ran 𝐺 ∈ V)
133132adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ran 𝐺 ∈ V)
134 simprr2 1219 . . . . . . . 8 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙)
13551rspccva 3607 . . . . . . . 8 ((∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
136134, 135sylan 578 . . . . . . 7 (((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) ∧ 𝑘 ∈ ran 𝐺) → (𝑔𝑘) ∈ 𝑘)
137 simprr3 1220 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → 𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
13870adantr 479 . . . . . . 7 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → (𝑇𝑈) ⊆ 𝑋)
139 stoweidlem35.1 . . . . . . . 8 𝑡𝜑
140 nfv 1910 . . . . . . . . 9 𝑡 𝑚 ∈ ℕ
141 nfcv 2892 . . . . . . . . . . 11 𝑡𝑔
142 nfcv 2892 . . . . . . . . . . . . . 14 𝑡𝑋
143 nfrab1 3439 . . . . . . . . . . . . . . . 16 𝑡{𝑡𝑇 ∣ 0 < (𝑡)}
144143nfeq2 2910 . . . . . . . . . . . . . . 15 𝑡 𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}
145 nfv 1910 . . . . . . . . . . . . . . . . . 18 𝑡(𝑍) = 0
146 nfra1 3272 . . . . . . . . . . . . . . . . . 18 𝑡𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1)
147145, 146nfan 1895 . . . . . . . . . . . . . . . . 17 𝑡((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))
148 nfcv 2892 . . . . . . . . . . . . . . . . 17 𝑡𝐴
149147, 148nfrabw 3457 . . . . . . . . . . . . . . . 16 𝑡{𝐴 ∣ ((𝑍) = 0 ∧ ∀𝑡𝑇 (0 ≤ (𝑡) ∧ (𝑡) ≤ 1))}
15080, 149nfcxfr 2890 . . . . . . . . . . . . . . 15 𝑡𝑄
151144, 150nfrabw 3457 . . . . . . . . . . . . . 14 𝑡{𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}}
152142, 151nfmpt 5260 . . . . . . . . . . . . 13 𝑡(𝑤𝑋 ↦ {𝑄𝑤 = {𝑡𝑇 ∣ 0 < (𝑡)}})
1532, 152nfcxfr 2890 . . . . . . . . . . . 12 𝑡𝐺
154153nfrn 5958 . . . . . . . . . . 11 𝑡ran 𝐺
155141, 154nffn 6659 . . . . . . . . . 10 𝑡 𝑔 Fn ran 𝐺
156 nfv 1910 . . . . . . . . . . 11 𝑡(𝑔𝑙) ∈ 𝑙
157154, 156nfralw 3299 . . . . . . . . . 10 𝑡𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
158 nfcv 2892 . . . . . . . . . . 11 𝑡𝑓
159 nfcv 2892 . . . . . . . . . . 11 𝑡(1...𝑚)
160158, 159, 154nff1o 6841 . . . . . . . . . 10 𝑡 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
161155, 157, 160nf3an 1897 . . . . . . . . 9 𝑡(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
162140, 161nfan 1895 . . . . . . . 8 𝑡(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
163139, 162nfan 1895 . . . . . . 7 𝑡(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
164 nfv 1910 . . . . . . . . 9 𝑤 𝑚 ∈ ℕ
165 nfcv 2892 . . . . . . . . . . 11 𝑤𝑔
166165, 11nffn 6659 . . . . . . . . . 10 𝑤 𝑔 Fn ran 𝐺
167 nfv 1910 . . . . . . . . . . 11 𝑤(𝑔𝑙) ∈ 𝑙
16811, 167nfralw 3299 . . . . . . . . . 10 𝑤𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙
169 nfcv 2892 . . . . . . . . . . 11 𝑤𝑓
170 nfcv 2892 . . . . . . . . . . 11 𝑤(1...𝑚)
171169, 170, 11nff1o 6841 . . . . . . . . . 10 𝑤 𝑓:(1...𝑚)–1-1-onto→ran 𝐺
172166, 168, 171nf3an 1897 . . . . . . . . 9 𝑤(𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)
173164, 172nfan 1895 . . . . . . . 8 𝑤(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))
1748, 173nfan 1895 . . . . . . 7 𝑤(𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)))
1752, 128, 129, 130, 133, 136, 137, 138, 163, 174, 84stoweidlem27 45648 . . . . . 6 ((𝜑 ∧ (𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
176175ex 411 . . . . 5 (𝜑 → ((𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
1771762eximdv 1915 . . . 4 (𝜑 → (∃𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
178177eximdv 1913 . . 3 (𝜑 → (∃𝑚𝑔𝑓(𝑚 ∈ ℕ ∧ (𝑔 Fn ran 𝐺 ∧ ∀𝑙 ∈ ran 𝐺(𝑔𝑙) ∈ 𝑙𝑓:(1...𝑚)–1-1-onto→ran 𝐺)) → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡)))))
179127, 178mpd 15 . 2 (𝜑 → ∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
180 id 22 . . . 4 (∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
181180exlimivv 1928 . . 3 (∃𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
182181eximi 1830 . 2 (∃𝑚𝑔𝑓𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))) → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
183179, 182syl 17 1 (𝜑 → ∃𝑚𝑞(𝑚 ∈ ℕ ∧ (𝑞:(1...𝑚)⟶𝑄 ∧ ∀𝑡 ∈ (𝑇𝑈)∃𝑖 ∈ (1...𝑚)0 < ((𝑞𝑖)‘𝑡))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  w3a 1084  wal 1532   = wceq 1534  wex 1774  wnf 1778  wcel 2099  wne 2930  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cdif 3944  wss 3947  c0 4325   cuni 4913   class class class wbr 5153  cmpt 5236  dom cdm 5682  ran crn 5683   Fn wfn 6549  wf 6550  1-1-ontowf1o 6553  cfv 6554  (class class class)co 7424  Fincfn 8974  0cc0 11158  1c1 11159   < clt 11298  cle 11299  cn 12264  ...cfz 13538  chash 14347
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 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-nn 12265  df-n0 12525  df-z 12611  df-uz 12875  df-fz 13539  df-hash 14348
This theorem is referenced by:  stoweidlem53  45674
  Copyright terms: Public domain W3C validator