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	⊢ ( 𝜑 → ( 𝑇 ∖ 𝑈 ) ⊆ ∪ 𝑊 )