Metamath Proof Explorer

Theorem stoweidlem35

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 ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses 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 stoweidlem35 ( 𝜑 → ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem35.1 ⊢ Ⅎ 𝑡 𝜑
2 stoweidlem35.2 ⊢ Ⅎ 𝑤 𝜑
3 stoweidlem35.3 ⊢ Ⅎ ℎ 𝜑
4 stoweidlem35.4 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
5 stoweidlem35.5 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
6 stoweidlem35.6 ⊢ 𝐺 = ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
7 stoweidlem35.7 ⊢ ( 𝜑 → 𝐴 ∈ V )
8 stoweidlem35.8 ⊢ ( 𝜑 → 𝑋 ∈ Fin )
9 stoweidlem35.9 ⊢ ( 𝜑 → 𝑋 ⊆ 𝑊 )
10 stoweidlem35.10 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑋 )
11 stoweidlem35.11 ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ≠ ∅ )
12 6 rnmptfi ⊢ ( 𝑋 ∈ Fin → ran 𝐺 ∈ Fin )
13 8 12 syl ⊢ ( 𝜑 → ran 𝐺 ∈ Fin )
14 fnchoice ⊢ ( ran 𝐺 ∈ Fin → ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) )
15 14 adantl ⊢ ( ( 𝜑 ∧ ran 𝐺 ∈ Fin ) → ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) → 𝑔 Fn ran 𝐺 )
17 nfmpt1 ⊢ Ⅎ 𝑤 ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
18 6 17 nfcxfr ⊢ Ⅎ 𝑤 𝐺
19 18 nfrn ⊢ Ⅎ 𝑤 ran 𝐺
20 19 nfcri ⊢ Ⅎ 𝑤 𝑘 ∈ ran 𝐺
21 2 20 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑘 ∈ ran 𝐺 )
22 9 sselda ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ 𝑊 )
23 22 5 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → 𝑤 ∈ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
24 rabid ⊢ ( 𝑤 ∈ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ( 𝑤 ∈ 𝐽 ∧ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
25 23 24 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ( 𝑤 ∈ 𝐽 ∧ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
26 25 simprd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } )
27 df-rex ⊢ ( ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ ∃ ℎ ( ℎ ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
28 26 27 sylib ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
29 rabid ⊢ ( ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ( ℎ ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
30 29 exbii ⊢ ( ∃ ℎ ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ∃ ℎ ( ℎ ∈ 𝑄 ∧ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
31 28 30 sylibr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → ∃ ℎ ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
32 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ∃ ℎ ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
33 nfv ⊢ Ⅎ ℎ 𝑤 ∈ 𝑋
34 3 33 nfan ⊢ Ⅎ ℎ ( 𝜑 ∧ 𝑤 ∈ 𝑋 )
35 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
36 35 nfeq2 ⊢ Ⅎ ℎ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
37 34 36 nfan ⊢ Ⅎ ℎ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
38 eleq2 ⊢ ( 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } → ( ℎ ∈ 𝑘 ↔ ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) )
39 38 biimprd ⊢ ( 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } → ( ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } → ℎ ∈ 𝑘 ) )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } → ℎ ∈ 𝑘 ) )
41 37 40 eximd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ( ∃ ℎ ℎ ∈ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } → ∃ ℎ ℎ ∈ 𝑘 ) )
42 32 41 mpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ∃ ℎ ℎ ∈ 𝑘 )
43 42 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ran 𝐺 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) → ∃ ℎ ℎ ∈ 𝑘 )
44 6 elrnmpt ⊢ ( 𝑘 ∈ ran 𝐺 → ( 𝑘 ∈ ran 𝐺 ↔ ∃ 𝑤 ∈ 𝑋 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ) )
45 44 ibi ⊢ ( 𝑘 ∈ ran 𝐺 → ∃ 𝑤 ∈ 𝑋 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
46 45 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝐺 ) → ∃ 𝑤 ∈ 𝑋 𝑘 = { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
47 21 43 46 r19.29af ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝐺 ) → ∃ ℎ ℎ ∈ 𝑘 )
48 n0 ⊢ ( 𝑘 ≠ ∅ ↔ ∃ ℎ ℎ ∈ 𝑘 )
49 47 48 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ran 𝐺 ) → 𝑘 ≠ ∅ )
50 49 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) ∧ 𝑘 ∈ ran 𝐺 ) → 𝑘 ≠ ∅ )
51 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) ∧ 𝑘 ∈ ran 𝐺 ) → ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
52 neeq1 ⊢ ( 𝑙 = 𝑘 → ( 𝑙 ≠ ∅ ↔ 𝑘 ≠ ∅ ) )
53 fveq2 ⊢ ( 𝑙 = 𝑘 → ( 𝑔 ‘ 𝑙 ) = ( 𝑔 ‘ 𝑘 ) )
54 53 eleq1d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑔 ‘ 𝑘 ) ∈ 𝑙 ) )
55 eleq2 ⊢ ( 𝑙 = 𝑘 → ( ( 𝑔 ‘ 𝑘 ) ∈ 𝑙 ↔ ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ) )
56 54 55 bitrd ⊢ ( 𝑙 = 𝑘 → ( ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ↔ ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ) )
57 52 56 imbi12d ⊢ ( 𝑙 = 𝑘 → ( ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ↔ ( 𝑘 ≠ ∅ → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ) ) )
58 57 rspccva ⊢ ( ( ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑘 ∈ ran 𝐺 ) → ( 𝑘 ≠ ∅ → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ) )
59 51 58 sylancom ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) ∧ 𝑘 ∈ ran 𝐺 ) → ( 𝑘 ≠ ∅ → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ) )
60 50 59 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) ∧ 𝑘 ∈ ran 𝐺 ) → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 )
61 60 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) → ∀ 𝑘 ∈ ran 𝐺 ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 )
62 fveq2 ⊢ ( 𝑘 = 𝑙 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 𝑙 ) )
63 62 eleq1d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ↔ ( 𝑔 ‘ 𝑙 ) ∈ 𝑘 ) )
64 eleq2 ⊢ ( 𝑘 = 𝑙 → ( ( 𝑔 ‘ 𝑙 ) ∈ 𝑘 ↔ ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
65 63 64 bitrd ⊢ ( 𝑘 = 𝑙 → ( ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ↔ ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
66 65 cbvralvw ⊢ ( ∀ 𝑘 ∈ ran 𝐺 ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 ↔ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 )
67 61 66 sylib ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) → ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 )
68 16 67 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) ) → ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
69 68 ex ⊢ ( 𝜑 → ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) → ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ ran 𝐺 ∈ Fin ) → ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) → ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) )
71 70 eximdv ⊢ ( ( 𝜑 ∧ ran 𝐺 ∈ Fin ) → ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑙 ≠ ∅ → ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) → ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ) )
72 15 71 mpd ⊢ ( ( 𝜑 ∧ ran 𝐺 ∈ Fin ) → ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
73 13 72 mpdan ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
74 73 ralrimivw ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) )
75 ssn0 ⊢ ( ( ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑋 ∧ ( 𝑇 ∖ 𝑈 ) ≠ ∅ ) → ∪ 𝑋 ≠ ∅ )
76 10 11 75 syl2anc ⊢ ( 𝜑 → ∪ 𝑋 ≠ ∅ )
77 76 neneqd ⊢ ( 𝜑 → ¬ ∪ 𝑋 = ∅ )
78 unieq ⊢ ( 𝑋 = ∅ → ∪ 𝑋 = ∪ ∅ )
79 uni0 ⊢ ∪ ∅ = ∅
80 78 79 eqtrdi ⊢ ( 𝑋 = ∅ → ∪ 𝑋 = ∅ )
81 77 80 nsyl ⊢ ( 𝜑 → ¬ 𝑋 = ∅ )
82 dm0rn0 ⊢ ( dom 𝐺 = ∅ ↔ ran 𝐺 = ∅ )
83 4 7 rabexd ⊢ ( 𝜑 → 𝑄 ∈ V )
84 nfrab1 ⊢ Ⅎ ℎ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
85 4 84 nfcxfr ⊢ Ⅎ ℎ 𝑄
86 85 rabexgf ⊢ ( 𝑄 ∈ V → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
87 83 86 syl ⊢ ( 𝜑 → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑋 ) → { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ∈ V )
89 2 88 6 fmptdf ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ V )
90 dffn2 ⊢ ( 𝐺 Fn 𝑋 ↔ 𝐺 : 𝑋 ⟶ V )
91 89 90 sylibr ⊢ ( 𝜑 → 𝐺 Fn 𝑋 )
92 91 fndmd ⊢ ( 𝜑 → dom 𝐺 = 𝑋 )
93 92 eqeq1d ⊢ ( 𝜑 → ( dom 𝐺 = ∅ ↔ 𝑋 = ∅ ) )
94 82 93 bitr3id ⊢ ( 𝜑 → ( ran 𝐺 = ∅ ↔ 𝑋 = ∅ ) )
95 81 94 mtbird ⊢ ( 𝜑 → ¬ ran 𝐺 = ∅ )
96 fz1f1o ⊢ ( ran 𝐺 ∈ Fin → ( ran 𝐺 = ∅ ∨ ( ( ♯ ‘ ran 𝐺 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) ) )
97 13 96 syl ⊢ ( 𝜑 → ( ran 𝐺 = ∅ ∨ ( ( ♯ ‘ ran 𝐺 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) ) )
98 97 ord ⊢ ( 𝜑 → ( ¬ ran 𝐺 = ∅ → ( ( ♯ ‘ ran 𝐺 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) ) )
99 95 98 mpd ⊢ ( 𝜑 → ( ( ♯ ‘ ran 𝐺 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) )
100 oveq2 ⊢ ( 𝑚 = ( ♯ ‘ ran 𝐺 ) → ( 1 ... 𝑚 ) = ( 1 ... ( ♯ ‘ ran 𝐺 ) ) )
101 100 f1oeq2d ⊢ ( 𝑚 = ( ♯ ‘ ran 𝐺 ) → ( 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ↔ 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) )
102 101 exbidv ⊢ ( 𝑚 = ( ♯ ‘ ran 𝐺 ) → ( ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ↔ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) )
103 102 rspcev ⊢ ( ( ( ♯ ‘ ran 𝐺 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ ran 𝐺 ) ) –1-1-onto→ ran 𝐺 ) → ∃ 𝑚 ∈ ℕ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 )
104 99 103 syl ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 )
105 r19.29 ⊢ ( ( ∀ 𝑚 ∈ ℕ ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑚 ∈ ℕ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) → ∃ 𝑚 ∈ ℕ ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
106 74 104 105 syl2anc ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
107 exdistrv ⊢ ( ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ↔ ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
108 107 biimpri ⊢ ( ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) → ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
109 108 a1i ⊢ ( 𝜑 → ( ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) → ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
110 109 reximdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ℕ ( ∃ 𝑔 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ ∃ 𝑓 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) → ∃ 𝑚 ∈ ℕ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
111 106 110 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∈ ℕ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
112 df-rex ⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ↔ ∃ 𝑚 ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
113 111 112 sylib ⊢ ( 𝜑 → ∃ 𝑚 ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
114 ax-5 ⊢ ( 𝑚 ∈ ℕ → ∀ 𝑔 𝑚 ∈ ℕ )
115 19.29 ⊢ ( ( ∀ 𝑔 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ( 𝑚 ∈ ℕ ∧ ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
116 114 115 sylan ⊢ ( ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ( 𝑚 ∈ ℕ ∧ ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
117 ax-5 ⊢ ( 𝑚 ∈ ℕ → ∀ 𝑓 𝑚 ∈ ℕ )
118 19.29 ⊢ ( ( ∀ 𝑓 𝑚 ∈ ℕ ∧ ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
119 117 118 sylan ⊢ ( ( 𝑚 ∈ ℕ ∧ ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
120 119 eximi ⊢ ( ∃ 𝑔 ( 𝑚 ∈ ℕ ∧ ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
121 116 120 syl ⊢ ( ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
122 df-3an ⊢ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ↔ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
123 122 anbi2i ⊢ ( ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ↔ ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
124 123 2exbii ⊢ ( ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ↔ ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
125 121 124 sylibr ⊢ ( ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
126 125 a1i ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) )
127 126 eximdv ⊢ ( 𝜑 → ( ∃ 𝑚 ( 𝑚 ∈ ℕ ∧ ∃ 𝑔 ∃ 𝑓 ( ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ) ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) )
128 113 127 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
129 83 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → 𝑄 ∈ V )
130 simprl ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → 𝑚 ∈ ℕ )
131 simprr1 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → 𝑔 Fn ran 𝐺 )
132 elex ⊢ ( ran 𝐺 ∈ Fin → ran 𝐺 ∈ V )
133 13 132 syl ⊢ ( 𝜑 → ran 𝐺 ∈ V )
134 133 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → ran 𝐺 ∈ V )
135 simprr2 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 )
136 56 rspccva ⊢ ( ( ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑘 ∈ ran 𝐺 ) → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 )
137 135 136 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) ∧ 𝑘 ∈ ran 𝐺 ) → ( 𝑔 ‘ 𝑘 ) ∈ 𝑘 )
138 simprr3 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 )
139 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑋 )
140 nfv ⊢ Ⅎ 𝑡 𝑚 ∈ ℕ
141 nfcv ⊢ Ⅎ 𝑡 𝑔
142 nfcv ⊢ Ⅎ 𝑡 𝑋
143 nfrab1 ⊢ Ⅎ 𝑡 { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
144 143 nfeq2 ⊢ Ⅎ 𝑡 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) }
145 nfv ⊢ Ⅎ 𝑡 ( ℎ ‘ 𝑍 ) = 0
146 nfra1 ⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 )
147 145 146 nfan ⊢ Ⅎ 𝑡 ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) )
148 nfcv ⊢ Ⅎ 𝑡 𝐴
149 147 148 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
150 4 149 nfcxfr ⊢ Ⅎ 𝑡 𝑄
151 144 150 nfrabw ⊢ Ⅎ 𝑡 { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
152 142 151 nfmpt ⊢ Ⅎ 𝑡 ( 𝑤 ∈ 𝑋 ↦ { ℎ ∈ 𝑄 ∣ 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
153 6 152 nfcxfr ⊢ Ⅎ 𝑡 𝐺
154 153 nfrn ⊢ Ⅎ 𝑡 ran 𝐺
155 141 154 nffn ⊢ Ⅎ 𝑡 𝑔 Fn ran 𝐺
156 nfv ⊢ Ⅎ 𝑡 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙
157 154 156 nfralw ⊢ Ⅎ 𝑡 ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙
158 nfcv ⊢ Ⅎ 𝑡 𝑓
159 nfcv ⊢ Ⅎ 𝑡 ( 1 ... 𝑚 )
160 158 159 154 nff1o ⊢ Ⅎ 𝑡 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺
161 155 157 160 nf3an ⊢ Ⅎ 𝑡 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 )
162 140 161 nfan ⊢ Ⅎ 𝑡 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
163 1 162 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
164 nfv ⊢ Ⅎ 𝑤 𝑚 ∈ ℕ
165 nfcv ⊢ Ⅎ 𝑤 𝑔
166 165 19 nffn ⊢ Ⅎ 𝑤 𝑔 Fn ran 𝐺
167 nfv ⊢ Ⅎ 𝑤 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙
168 19 167 nfralw ⊢ Ⅎ 𝑤 ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙
169 nfcv ⊢ Ⅎ 𝑤 𝑓
170 nfcv ⊢ Ⅎ 𝑤 ( 1 ... 𝑚 )
171 169 170 19 nff1o ⊢ Ⅎ 𝑤 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺
172 166 168 171 nf3an ⊢ Ⅎ 𝑤 ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 )
173 164 172 nfan ⊢ Ⅎ 𝑤 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) )
174 2 173 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) )
175 6 129 130 131 134 137 138 139 163 174 85 stoweidlem27 ⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) ) → ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
176 175 ex ⊢ ( 𝜑 → ( ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
177 176 2eximdv ⊢ ( 𝜑 → ( ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑔 ∃ 𝑓 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
178 177 eximdv ⊢ ( 𝜑 → ( ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ( 𝑚 ∈ ℕ ∧ ( 𝑔 Fn ran 𝐺 ∧ ∀ 𝑙 ∈ ran 𝐺 ( 𝑔 ‘ 𝑙 ) ∈ 𝑙 ∧ 𝑓 : ( 1 ... 𝑚 ) –1-1-onto→ ran 𝐺 ) ) → ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) ) )
179 128 178 mpd ⊢ ( 𝜑 → ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
180 id ⊢ ( ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
181 180 exlimivv ⊢ ( ∃ 𝑔 ∃ 𝑓 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
182 181 eximi ⊢ ( ∃ 𝑚 ∃ 𝑔 ∃ 𝑓 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) → ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )
183 179 182 syl ⊢ ( 𝜑 → ∃ 𝑚 ∃ 𝑞 ( 𝑚 ∈ ℕ ∧ ( 𝑞 : ( 1 ... 𝑚 ) ⟶ 𝑄 ∧ ∀ 𝑡 ∈ ( 𝑇 ∖ 𝑈 ) ∃ 𝑖 ∈ ( 1 ... 𝑚 ) 0 < ( ( 𝑞 ‘ 𝑖 ) ‘ 𝑡 ) ) ) )