Theorem iunhoiioo

Description: A n-dimensional open interval expressed as the indexed union of half-open intervals. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	iunhoiioo.k	⊢ Ⅎ 𝑘 𝜑
	iunhoiioo.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	iunhoiioo.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
	iunhoiioo.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
Assertion	iunhoiioo	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		iunhoiioo.k	⊢ Ⅎ 𝑘 𝜑
2		iunhoiioo.x	⊢ ( 𝜑 → 𝑋 ∈ Fin )
3		iunhoiioo.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
4		iunhoiioo.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
5		nnn0	⊢ ℕ ≠ ∅
6		iunconst	⊢ ( ℕ ≠ ∅ → ∪ 𝑛 ∈ ℕ { ∅ } = { ∅ } )
7	5 6	ax-mp	⊢ ∪ 𝑛 ∈ ℕ { ∅ } = { ∅ }
8	7	a1i	⊢ ( 𝑋 = ∅ → ∪ 𝑛 ∈ ℕ { ∅ } = { ∅ } )
9		ixpeq1	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ ∅ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
10		ixp0x	⊢ X 𝑘 ∈ ∅ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = { ∅ }
11	10	a1i	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ ∅ ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = { ∅ } )
12	9 11	eqtrd	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = { ∅ } )
13	12	adantr	⊢ ( ( 𝑋 = ∅ ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = { ∅ } )
14	13	iuneq2dv	⊢ ( 𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = ∪ 𝑛 ∈ ℕ { ∅ } )
15		ixpeq1	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) = X 𝑘 ∈ ∅ ( 𝐴 (,) 𝐵 ) )
16		ixp0x	⊢ X 𝑘 ∈ ∅ ( 𝐴 (,) 𝐵 ) = { ∅ }
17	16	a1i	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ ∅ ( 𝐴 (,) 𝐵 ) = { ∅ } )
18	15 17	eqtrd	⊢ ( 𝑋 = ∅ → X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) = { ∅ } )
19	8 14 18	3eqtr4d	⊢ ( 𝑋 = ∅ → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
20	19	adantl	⊢ ( ( 𝜑 ∧ 𝑋 = ∅ ) → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
21		nfv	⊢ Ⅎ 𝑘 𝑛 ∈ ℕ
22	1 21	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑛 ∈ ℕ )
23	3	rexrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
24	23	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ* )
25	4	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
26	3	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
27		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
28	27	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝑛 ∈ ℝ+ )
29	28	rpreccld	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( 1 / 𝑛 ) ∈ ℝ+ )
30	26 29	ltaddrpd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 < ( 𝐴 + ( 1 / 𝑛 ) ) )
31	4	xrleidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ≤ 𝐵 )
32	31	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ≤ 𝐵 )
33		icossioo	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 < ( 𝐴 + ( 1 / 𝑛 ) ) ∧ 𝐵 ≤ 𝐵 ) ) → ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
34	24 25 30 32 33	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 ∈ 𝑋 ) → ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ ( 𝐴 (,) 𝐵 ) )
35	22 34	ixpssixp	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
36	35	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
37		iunss	⊢ ( ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ↔ ∀ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
38	36 37	sylibr	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
39	38	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) ⊆ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
40		nfv	⊢ Ⅎ 𝑘 ¬ 𝑋 = ∅
41	1 40	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ ¬ 𝑋 = ∅ )
42		nfcv	⊢ Ⅎ 𝑘 𝑓
43		nfixp1	⊢ Ⅎ 𝑘 X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 )
44	42 43	nfel	⊢ Ⅎ 𝑘 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 )
45	41 44	nfan	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
46	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) → 𝑋 ∈ Fin )
47		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
48	47	ad2antlr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) → 𝑋 ≠ ∅ )
49	3	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐴 ∈ ℝ )
50	4	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) ∧ 𝑘 ∈ 𝑋 ) → 𝐵 ∈ ℝ* )
51		simpr	⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) → 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
52		eqid	⊢ inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝑓 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < ) = inf ( ran ( 𝑘 ∈ 𝑋 ↦ ( ( 𝑓 ‘ 𝑘 ) − 𝐴 ) ) , ℝ , < )
53	45 46 48 49 50 51 52	iunhoiioolem	⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) ∧ 𝑓 ∈ X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) ) → 𝑓 ∈ ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) )
54	39 53	eqelssd	⊢ ( ( 𝜑 ∧ ¬ 𝑋 = ∅ ) → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )
55	20 54	pm2.61dan	⊢ ( 𝜑 → ∪ 𝑛 ∈ ℕ X 𝑘 ∈ 𝑋 ( ( 𝐴 + ( 1 / 𝑛 ) ) [,) 𝐵 ) = X 𝑘 ∈ 𝑋 ( 𝐴 (,) 𝐵 ) )