ioondisj1

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

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

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		simprl	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → 𝐴 ≤ 𝐶 )
8	7	iftrued	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) = 𝐶 )
9	8	oveq1d	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) = ( 𝐶 (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )
10		simprr	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → 𝐶 < 𝐵 )
11		simplr3	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → 𝐶 < 𝐷 )
12	10 11	jca	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( 𝐶 < 𝐵 ∧ 𝐶 < 𝐷 ) )
13		xrltmin	⊢ ( ( 𝐶 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ) → ( 𝐶 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝐶 < 𝐵 ∧ 𝐶 < 𝐷 ) ) )
14	3 2 4 13	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( 𝐶 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ↔ ( 𝐶 < 𝐵 ∧ 𝐶 < 𝐷 ) ) )
15	12 14	mpbird	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → 𝐶 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) )
16	2 4	ifcld	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ∈ ℝ^* )
17		ioon0	⊢ ( ( 𝐶 ∈ ℝ^* ∧ if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ∈ ℝ^* ) → ( ( 𝐶 (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ≠ ∅ ↔ 𝐶 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )
18	3 16 17	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( ( 𝐶 (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ≠ ∅ ↔ 𝐶 < if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) )
19	15 18	mpbird	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( 𝐶 (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ≠ ∅ )
20	9 19	eqnetrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( if ( 𝐴 ≤ 𝐶 , 𝐶 , 𝐴 ) (,) if ( 𝐵 ≤ 𝐷 , 𝐵 , 𝐷 ) ) ≠ ∅ )
21	6 20	eqnetrd	⊢ ( ( ( ( 𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝐴 < 𝐵 ) ∧ ( 𝐶 ∈ ℝ^* ∧ 𝐷 ∈ ℝ^* ∧ 𝐶 < 𝐷 ) ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) → ( ( 𝐴 (,) 𝐵 ) ∩ ( 𝐶 (,) 𝐷 ) ) ≠ ∅ )

Metamath Proof Explorer

Theorem ioondisj1

Proof