Metamath Proof Explorer


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 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 ( 𝐵𝐷 , 𝐵 , 𝐷 ) ) )