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	bitr4di	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐶 ∈ ℝ^* ) ∧ ( 𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ) ) ∧ 𝑧 ∈ ℝ^* ) → ( ( 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 ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )

Metamath Proof Explorer

Theorem ixxin

Proof