Theorem ixxin

Description: Intersection of two intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Hypotheses	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
	ixxin.2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ↔ ( 𝐴 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ) )
	ixxin.3	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
Assertion	ixxin	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐶 𝑂 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑂 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		ixxin.2	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ↔ ( 𝐴 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ) )
3		ixxin.3	⊢ ( ( 𝑧 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
4		inrab	⊢ ( { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ∩ { 𝑧 ∈ ℝ* ∣ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) } ) = { 𝑧 ∈ ℝ* ∣ ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ∧ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) ) }
5	1	ixxval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )
6	1	ixxval	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝐶 𝑂 𝐷 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) } )
7	5 6	ineqan12d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐶 𝑂 𝐷 ) ) = ( { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ∩ { 𝑧 ∈ ℝ* ∣ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) } ) )
8	2	ad4ant124	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝑧 ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ↔ ( 𝐴 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ) )
9	3	3expb	⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
10	9	ancoms	⊢ ( ( ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ∧ 𝑧 ∈ ℝ* ) → ( 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
11	10	adantll	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝑧 ∈ ℝ* ) → ( 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
12	8 11	anbi12d	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝑧 ∈ ℝ* ) → ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ↔ ( ( 𝐴 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ∧ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) ) )
13		an4	⊢ ( ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ∧ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) ) ↔ ( ( 𝐴 𝑅 𝑧 ∧ 𝐶 𝑅 𝑧 ) ∧ ( 𝑧 𝑆 𝐵 ∧ 𝑧 𝑆 𝐷 ) ) )
14	12 13	syl6bbr	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) ∧ 𝑧 ∈ ℝ* ) → ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ↔ ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ∧ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) ) ) )
15	14	rabbidva	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } = { 𝑧 ∈ ℝ* ∣ ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ∧ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) ) } )
16	15	an4s	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } = { 𝑧 ∈ ℝ* ∣ ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ∧ ( 𝐶 𝑅 𝑧 ∧ 𝑧 𝑆 𝐷 ) ) } )
17	4 7 16	3eqtr4a	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐶 𝑂 𝐷 ) ) = { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } )
18		ifcl	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) ∈ ℝ* )
19	18	ancoms	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) ∈ ℝ* )
20		ifcl	⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ∈ ℝ* )
21	1	ixxval	⊢ ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) ∈ ℝ* ∧ if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ∈ ℝ* ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑂 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) = { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } )
22	19 20 21	syl2an	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐵 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑂 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) = { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } )
23	22	an4s	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑂 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) = { 𝑧 ∈ ℝ* ∣ ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑅 𝑧 ∧ 𝑧 𝑆 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) } )
24	17 23	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) ) → ( ( 𝐴 𝑂 𝐵 ) ∩ ( 𝐶 𝑂 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) 𝑂 if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )