Metamath Proof Explorer

Theorem stoweidlem46

Description: This lemma proves that sets U(t) as defined in Lemma 1 of BrosowskiDeutsh p. 90, are a cover of T \ U. Using this lemma, in a later theorem we will prove that a finite subcover exists. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem46.1 ⊢ Ⅎ 𝑡 𝑈
stoweidlem46.2 ⊢ Ⅎ ℎ 𝑄
stoweidlem46.3 ⊢ Ⅎ 𝑞 𝜑
stoweidlem46.4 ⊢ Ⅎ 𝑡 𝜑
stoweidlem46.5 ⊢ 𝐾 = ( topGen ‘ ran (,) )
stoweidlem46.6 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
stoweidlem46.7 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
stoweidlem46.8 ⊢ 𝑇 = ∪ 𝐽
stoweidlem46.9 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
stoweidlem46.10 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
stoweidlem46.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem46.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
stoweidlem46.13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
stoweidlem46.14 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
stoweidlem46.15 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
stoweidlem46.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
stoweidlem46.17 ⊢ ( 𝜑 → 𝑇 ∈ V )
Assertion stoweidlem46 ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 )

Proof

Step Hyp Ref Expression
1 stoweidlem46.1 ⊢ Ⅎ 𝑡 𝑈
2 stoweidlem46.2 ⊢ Ⅎ ℎ 𝑄
3 stoweidlem46.3 ⊢ Ⅎ 𝑞 𝜑
4 stoweidlem46.4 ⊢ Ⅎ 𝑡 𝜑
5 stoweidlem46.5 ⊢ 𝐾 = ( topGen ‘ ran (,) )
6 stoweidlem46.6 ⊢ 𝑄 = { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) }
7 stoweidlem46.7 ⊢ 𝑊 = { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
8 stoweidlem46.8 ⊢ 𝑇 = ∪ 𝐽
9 stoweidlem46.9 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
10 stoweidlem46.10 ⊢ ( 𝜑 → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
11 stoweidlem46.11 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
12 stoweidlem46.12 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
13 stoweidlem46.13 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
14 stoweidlem46.14 ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
15 stoweidlem46.15 ⊢ ( 𝜑 → 𝑈 ∈ 𝐽 )
16 stoweidlem46.16 ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
17 stoweidlem46.17 ⊢ ( 𝜑 → 𝑇 ∈ V )
18 nfv ⊢ Ⅎ 𝑞 𝑠 ∈ ( 𝑇 ∖ 𝑈 )
19 3 18 nfan ⊢ Ⅎ 𝑞 ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) )
20 nfcv ⊢ Ⅎ 𝑡 𝑇
21 20 1 nfdif ⊢ Ⅎ 𝑡 ( 𝑇 ∖ 𝑈 )
22 21 nfel2 ⊢ Ⅎ 𝑡 𝑠 ∈ ( 𝑇 ∖ 𝑈 )
23 4 22 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) )
24 9 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐽 ∈ Comp )
25 10 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
26 11 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) + ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
27 12 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) → ( 𝑡 ∈ 𝑇 ↦ ( ( 𝑓 ‘ 𝑡 ) · ( 𝑔 ‘ 𝑡 ) ) ) ∈ 𝐴 )
28 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑡 ∈ 𝑇 ↦ 𝑥 ) ∈ 𝐴 )
29 14 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑟 ∈ 𝑇 ∧ 𝑡 ∈ 𝑇 ∧ 𝑟 ≠ 𝑡 ) ) → ∃ 𝑞 ∈ 𝐴 ( 𝑞 ‘ 𝑟 ) ≠ ( 𝑞 ‘ 𝑡 ) )
30 15 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑈 ∈ 𝐽 )
31 16 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑍 ∈ 𝑈 )
32 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) )
33 19 23 2 5 6 8 24 25 26 27 28 29 30 31 32 stoweidlem43 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑠 ) ) )
34 nfv ⊢ Ⅎ 𝑔 ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑠 ) )
35 2 nfel2 ⊢ Ⅎ ℎ 𝑔 ∈ 𝑄
36 nfv ⊢ Ⅎ ℎ 0 < ( 𝑔 ‘ 𝑠 )
37 35 36 nfan ⊢ Ⅎ ℎ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) )
38 eleq1 ⊢ ( ℎ = 𝑔 → ( ℎ ∈ 𝑄 ↔ 𝑔 ∈ 𝑄 ) )
39 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑠 ) = ( 𝑔 ‘ 𝑠 ) )
40 39 breq2d ⊢ ( ℎ = 𝑔 → ( 0 < ( ℎ ‘ 𝑠 ) ↔ 0 < ( 𝑔 ‘ 𝑠 ) ) )
41 38 40 anbi12d ⊢ ( ℎ = 𝑔 → ( ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑠 ) ) ↔ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) )
42 34 37 41 cbvexv1 ⊢ ( ∃ ℎ ( ℎ ∈ 𝑄 ∧ 0 < ( ℎ ‘ 𝑠 ) ) ↔ ∃ 𝑔 ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) )
43 33 42 sylib ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑔 ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) )
44 rabexg ⊢ ( 𝑇 ∈ V → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ V )
45 17 44 syl ⊢ ( 𝜑 → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ V )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ V )
47 eldifi ⊢ ( 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) → 𝑠 ∈ 𝑇 )
48 47 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → 𝑠 ∈ 𝑇 )
49 simprr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → 0 < ( 𝑔 ‘ 𝑠 ) )
50 fveq2 ⊢ ( 𝑡 = 𝑠 → ( 𝑔 ‘ 𝑡 ) = ( 𝑔 ‘ 𝑠 ) )
51 50 breq2d ⊢ ( 𝑡 = 𝑠 → ( 0 < ( 𝑔 ‘ 𝑡 ) ↔ 0 < ( 𝑔 ‘ 𝑠 ) ) )
52 51 elrab ⊢ ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ↔ ( 𝑠 ∈ 𝑇 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) )
53 48 49 52 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } )
54 simpll ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → 𝜑 )
55 10 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → 𝐴 ⊆ ( 𝐽 Cn 𝐾 ) )
56 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → 𝑔 ∈ 𝑄 )
57 56 6 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → 𝑔 ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } )
58 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑍 ) = ( 𝑔 ‘ 𝑍 ) )
59 58 eqeq1d ⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 𝑍 ) = 0 ↔ ( 𝑔 ‘ 𝑍 ) = 0 ) )
60 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 𝑡 ) = ( 𝑔 ‘ 𝑡 ) )
61 60 breq2d ⊢ ( ℎ = 𝑔 → ( 0 ≤ ( ℎ ‘ 𝑡 ) ↔ 0 ≤ ( 𝑔 ‘ 𝑡 ) ) )
62 60 breq1d ⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 𝑡 ) ≤ 1 ↔ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) )
63 61 62 anbi12d ⊢ ( ℎ = 𝑔 → ( ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) )
64 63 ralbidv ⊢ ( ℎ = 𝑔 → ( ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ↔ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) )
65 59 64 anbi12d ⊢ ( ℎ = 𝑔 → ( ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) ↔ ( ( 𝑔 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) ) )
66 65 elrab ⊢ ( 𝑔 ∈ { ℎ ∈ 𝐴 ∣ ( ( ℎ ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( ℎ ‘ 𝑡 ) ∧ ( ℎ ‘ 𝑡 ) ≤ 1 ) ) } ↔ ( 𝑔 ∈ 𝐴 ∧ ( ( 𝑔 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) ) )
67 57 66 sylib ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → ( 𝑔 ∈ 𝐴 ∧ ( ( 𝑔 ‘ 𝑍 ) = 0 ∧ ∀ 𝑡 ∈ 𝑇 ( 0 ≤ ( 𝑔 ‘ 𝑡 ) ∧ ( 𝑔 ‘ 𝑡 ) ≤ 1 ) ) ) )
68 67 simpld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → 𝑔 ∈ 𝐴 )
69 55 68 sseldd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → 𝑔 ∈ ( 𝐽 Cn 𝐾 ) )
70 69 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → 𝑔 ∈ ( 𝐽 Cn 𝐾 ) )
71 nfcv ⊢ Ⅎ 𝑡 0
72 nfcv ⊢ Ⅎ 𝑡 𝑔
73 nfv ⊢ Ⅎ 𝑡 𝑔 ∈ ( 𝐽 Cn 𝐾 )
74 4 73 nfan ⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) )
75 eqid ⊢ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) }
76 0xr ⊢ 0 ∈ ℝ*
77 76 a1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ) → 0 ∈ ℝ* )
78 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝑔 ∈ ( 𝐽 Cn 𝐾 ) )
79 71 72 74 5 8 75 77 78 rfcnpre1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐽 Cn 𝐾 ) ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝐽 )
80 54 70 79 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝐽 )
81 eqidd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } )
82 nfv ⊢ Ⅎ ℎ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) }
83 nfcv ⊢ Ⅎ ℎ 𝑔
84 60 breq2d ⊢ ( ℎ = 𝑔 → ( 0 < ( ℎ ‘ 𝑡 ) ↔ 0 < ( 𝑔 ‘ 𝑡 ) ) )
85 84 rabbidv ⊢ ( ℎ = 𝑔 → { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } )
86 85 eqeq2d ⊢ ( ℎ = 𝑔 → ( { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ) )
87 82 83 2 86 rspcegf ⊢ ( ( 𝑔 ∈ 𝑄 ∧ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ) → ∃ ℎ ∈ 𝑄 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } )
88 56 81 87 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝑄 ) → ∃ ℎ ∈ 𝑄 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } )
89 88 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → ∃ ℎ ∈ 𝑄 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } )
90 eqeq1 ⊢ ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } → ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
91 90 rexbidv ⊢ ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } → ( ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ↔ ∃ ℎ ∈ 𝑄 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
92 91 elrab ⊢ ( { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } ↔ ( { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝐽 ∧ ∃ ℎ ∈ 𝑄 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } ) )
93 80 89 92 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } } )
94 93 7 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 )
95 nfcv ⊢ Ⅎ 𝑤 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) }
96 nfv ⊢ Ⅎ 𝑤 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) }
97 nfrab1 ⊢ Ⅎ 𝑤 { 𝑤 ∈ 𝐽 ∣ ∃ ℎ ∈ 𝑄 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( ℎ ‘ 𝑡 ) } }
98 7 97 nfcxfr ⊢ Ⅎ 𝑤 𝑊
99 98 nfel2 ⊢ Ⅎ 𝑤 { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊
100 96 99 nfan ⊢ Ⅎ 𝑤 ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∧ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 )
101 eleq2 ⊢ ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } → ( 𝑠 ∈ 𝑤 ↔ 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ) )
102 eleq1 ⊢ ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } → ( 𝑤 ∈ 𝑊 ↔ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 ) )
103 101 102 anbi12d ⊢ ( 𝑤 = { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } → ( ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) ↔ ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∧ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 ) ) )
104 95 100 103 spcegf ⊢ ( { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ V → ( ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∧ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) ) )
105 104 imp ⊢ ( ( { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ V ∧ ( 𝑠 ∈ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∧ { 𝑡 ∈ 𝑇 ∣ 0 < ( 𝑔 ‘ 𝑡 ) } ∈ 𝑊 ) ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) )
106 46 53 94 105 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) ∧ ( 𝑔 ∈ 𝑄 ∧ 0 < ( 𝑔 ‘ 𝑠 ) ) ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) )
107 43 106 exlimddv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) )
108 nfcv ⊢ Ⅎ 𝑤 𝑠
109 108 98 elunif ⊢ ( 𝑠 ∈ ∪ 𝑊 ↔ ∃ 𝑤 ( 𝑠 ∈ 𝑤 ∧ 𝑤 ∈ 𝑊 ) )
110 107 109 sylibr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) ) → 𝑠 ∈ ∪ 𝑊 )
111 110 ex ⊢ ( 𝜑 → ( 𝑠 ∈ ( 𝑇 ∖ 𝑈 ) → 𝑠 ∈ ∪ 𝑊 ) )
112 111 ssrdv ⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 )