Theorem icccmplem1

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 18-Jun-2014)

	Ref	Expression
Hypotheses	icccmp.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
	icccmp.2	⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
	icccmp.3	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
	icccmp.4	⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
	icccmp.5	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	icccmp.6	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	icccmp.7	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	icccmp.8	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
	icccmp.9	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
Assertion	icccmplem1	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		icccmp.1	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		icccmp.2	⊢ 𝑇 = ( 𝐽 ↾t ( 𝐴 [,] 𝐵 ) )
3		icccmp.3	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4		icccmp.4	⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 }
5		icccmp.5	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6		icccmp.6	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
7		icccmp.7	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
8		icccmp.8	⊢ ( 𝜑 → 𝑈 ⊆ 𝐽 )
9		icccmp.9	⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ∪ 𝑈 )
10	5	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
11	6	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
12		lbicc2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
13	10 11 7 12	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
14	9 13	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ∪ 𝑈 )
15		eluni2	⊢ ( 𝐴 ∈ ∪ 𝑈 ↔ ∃ 𝑢 ∈ 𝑈 𝐴 ∈ 𝑢 )
16	14 15	sylib	⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑈 𝐴 ∈ 𝑢 )
17		snssi	⊢ ( 𝑢 ∈ 𝑈 → { 𝑢 } ⊆ 𝑈 )
18	17	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → { 𝑢 } ⊆ 𝑈 )
19		snex	⊢ { 𝑢 } ∈ V
20	19	elpw	⊢ ( { 𝑢 } ∈ 𝒫 𝑈 ↔ { 𝑢 } ⊆ 𝑈 )
21	18 20	sylibr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → { 𝑢 } ∈ 𝒫 𝑈 )
22		snfi	⊢ { 𝑢 } ∈ Fin
23	22	a1i	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → { 𝑢 } ∈ Fin )
24	21 23	elind	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → { 𝑢 } ∈ ( 𝒫 𝑈 ∩ Fin ) )
25	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → 𝐴 ∈ ℝ* )
26		iccid	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
27	25 26	syl	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
28		snssi	⊢ ( 𝐴 ∈ 𝑢 → { 𝐴 } ⊆ 𝑢 )
29	28	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → { 𝐴 } ⊆ 𝑢 )
30	27 29	eqsstrd	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 )
31		unieq	⊢ ( 𝑧 = { 𝑢 } → ∪ 𝑧 = ∪ { 𝑢 } )
32		unisnv	⊢ ∪ { 𝑢 } = 𝑢
33	31 32	eqtrdi	⊢ ( 𝑧 = { 𝑢 } → ∪ 𝑧 = 𝑢 )
34	33	sseq2d	⊢ ( 𝑧 = { 𝑢 } → ( ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 ) )
35	34	rspcev	⊢ ( ( { 𝑢 } ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 )
36	24 30 35	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑈 ∧ 𝐴 ∈ 𝑢 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 )
37	16 36	rexlimddv	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 )
38		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝐴 [,] 𝑥 ) = ( 𝐴 [,] 𝐴 ) )
39	38	sseq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 ) )
40	39	rexbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ ∪ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 ) )
41	40 4	elrab2	⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ ∪ 𝑧 ) )
42	13 37 41	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
43	4	ssrab3	⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
44	43	sseli	⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
45		elicc2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
46	5 6 45	syl2anc	⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
47	46	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
48	47	simp3d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦 ≤ 𝐵 )
49	44 48	sylan2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ≤ 𝐵 )
50	49	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 )
51	42 50	jca	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝐵 ) )