Theorem icoreclin

Description: The set of closed-below, open-above intervals of reals is closed under finite intersection. (Contributed by ML, 27-Jul-2020)

	Ref	Expression
Hypothesis	isbasisrelowl.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion	icoreclin	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		isbasisrelowl.1	⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2	1	icoreelrnab	⊢ ( 𝑦 ∈ 𝐼 ↔ ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } )
3	1	icoreelrnab	⊢ ( 𝑥 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
4	1	isbasisrelowllem1	⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
5	4	ex	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
6	1	isbasisrelowllem2	⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
7	6	ex	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
8	5 7	jaod	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
9		incom	⊢ ( 𝑦 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑦 )
10	1	isbasisrelowllem2	⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑦 ∩ 𝑥 ) ∈ 𝐼 )
11	9 10	eqeltrrid	⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
12	11	ancom1s	⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
13	12	ex	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
14	1	isbasisrelowllem1	⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑦 ∩ 𝑥 ) ∈ 𝐼 )
15	9 14	eqeltrrid	⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ∧ ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
16	15	ancom1s	⊢ ( ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) ∧ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
17	16	ex	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
18	13 17	jaod	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
19		3simpa	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) → ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
20		3simpa	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) )
21		letric	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑎 ≤ 𝑐 ∨ 𝑐 ≤ 𝑎 ) )
22		letric	⊢ ( ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑏 ≤ 𝑑 ∨ 𝑑 ≤ 𝑏 ) )
23	21 22	anim12i	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( 𝑎 ≤ 𝑐 ∨ 𝑐 ≤ 𝑎 ) ∧ ( 𝑏 ≤ 𝑑 ∨ 𝑑 ≤ 𝑏 ) ) )
24		anddi	⊢ ( ( ( 𝑎 ≤ 𝑐 ∨ 𝑐 ≤ 𝑎 ) ∧ ( 𝑏 ≤ 𝑑 ∨ 𝑑 ≤ 𝑏 ) ) ↔ ( ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) ∨ ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) ) )
25	23 24	sylib	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑏 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) ∨ ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) ) )
26	25	an4s	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) ) → ( ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) ∨ ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) ) )
27	19 20 26	syl2an	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( ( ( 𝑎 ≤ 𝑐 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑎 ≤ 𝑐 ∧ 𝑑 ≤ 𝑏 ) ) ∨ ( ( 𝑐 ≤ 𝑎 ∧ 𝑏 ≤ 𝑑 ) ∨ ( 𝑐 ≤ 𝑎 ∧ 𝑑 ≤ 𝑏 ) ) ) )
28	8 18 27	mpjaod	⊢ ( ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ∧ ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )
29	28	ex	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) → ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
30	29	3expia	⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) ) )
31	30	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℝ ∃ 𝑏 ∈ ℝ 𝑥 = { 𝑧 ∈ ℝ ∣ ( 𝑎 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
32	3 31	sylbi	⊢ ( 𝑥 ∈ 𝐼 → ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
33	32	com12	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ∧ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } ) → ( 𝑥 ∈ 𝐼 → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
34	33	3expia	⊢ ( ( 𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } → ( 𝑥 ∈ 𝐼 → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) ) )
35	34	rexlimivv	⊢ ( ∃ 𝑐 ∈ ℝ ∃ 𝑑 ∈ ℝ 𝑦 = { 𝑧 ∈ ℝ ∣ ( 𝑐 ≤ 𝑧 ∧ 𝑧 < 𝑑 ) } → ( 𝑥 ∈ 𝐼 → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
36	2 35	sylbi	⊢ ( 𝑦 ∈ 𝐼 → ( 𝑥 ∈ 𝐼 → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 ) )
37	36	impcom	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐼 )