ioondisj2

Description: A condition for two open intervals not to be disjoint. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	ioondisj2	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		simpll1	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ^* )
2		simpll2	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ^* )
3		simplr1	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐶 ∈ ℝ^* )
4		simplr2	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐷 ∈ ℝ^* )
5		iooin	⊢ ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )
6	1 2 3 4 5	syl22anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )
7		simprr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐷 ≤ 𝐵 )
8		xrmineq	⊢ ( ( 𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐷 ≤ 𝐵 ) → if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) = 𝐷 )
9	2 4 7 8	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) = 𝐷 )
10	9	oveq2d	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) = ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) 𝐷 ) )
11		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ 𝐴 ≤ 𝐶 ) → 𝐴 ≤ 𝐶 )
12	11	iftrued	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ 𝐴 ≤ 𝐶 ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) = 𝐶 )
13		simplr3	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐶 < 𝐷 )
14	13	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ 𝐴 ≤ 𝐶 ) → 𝐶 < 𝐷 )
15	12 14	eqbrtrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ 𝐴 ≤ 𝐶 ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝐷 )
16		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝐶 ) → ¬ 𝐴 ≤ 𝐶 )
17	16	iffalsed	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝐶 ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) = 𝐴 )
18		simplrl	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝐶 ) → 𝐴 < 𝐷 )
19	17 18	eqbrtrd	⊢ ( ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) ∧ ¬ 𝐴 ≤ 𝐶 ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝐷 )
20	15 19	pm2.61dan	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝐷 )
21	3 1	ifcld	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) ∈ ℝ^* )
22		ioon0	⊢ ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ) → ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) 𝐷 ) ≠ ∅ ↔ if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝐷 ) )
23	21 4 22	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) 𝐷 ) ≠ ∅ ↔ if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) < 𝐷 ) )
24	20 23	mpbird	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) 𝐷 ) ≠ ∅ )
25	10 24	eqnetrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ≠ ∅ )
26	6 25	eqnetrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 < 𝐷 ∧ 𝐷 ≤ 𝐵 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ≠ ∅ )

Metamath Proof Explorer

Theorem ioondisj2

Proof