Theorem ioossioobi

Description: Biconditional form of ioossioo . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	ioossioobi.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	ioossioobi.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
	ioossioobi.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
	ioossioobi.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
	ioossioobi.cltd	⊢ ( 𝜑 → 𝐶 < 𝐷 )
Assertion	ioossioobi	⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ioossioobi.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		ioossioobi.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		ioossioobi.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4		ioossioobi.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
5		ioossioobi.cltd	⊢ ( 𝜑 → 𝐶 < 𝐷 )
6		simpr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
7		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
8	7	ixxssxr	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ*
9		infxrss	⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ* ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ≤ inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) )
10	6 8 9	sylancl	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ≤ inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
12	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
13		ioon0	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( ( 𝐶 (,) 𝐷 ) ≠ ∅ ↔ 𝐶 < 𝐷 ) )
14	3 4 13	syl2anc	⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ≠ ∅ ↔ 𝐶 < 𝐷 ) )
15	5 14	mpbird	⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ≠ ∅ )
16	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ≠ ∅ )
17		ssn0	⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
18	6 16 17	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
19		idd	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 < 𝐵 ) )
20		xrltle	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 ≤ 𝐵 ) )
21		idd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 < 𝑤 ) )
22		xrltle	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 ≤ 𝑤 ) )
23	7 19 20 21 22	ixxlb	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
24	11 12 18 23	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
25	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ* )
26	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ∈ ℝ* )
27		idd	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑤 < 𝐷 → 𝑤 < 𝐷 ) )
28		xrltle	⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑤 < 𝐷 → 𝑤 ≤ 𝐷 ) )
29		idd	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐶 < 𝑤 → 𝐶 < 𝑤 ) )
30		xrltle	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐶 < 𝑤 → 𝐶 ≤ 𝑤 ) )
31	7 27 28 29 30	ixxlb	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐶 )
32	25 26 16 31	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐶 )
33	10 24 32	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ≤ 𝐶 )
34		supxrss	⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ* ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) ≤ sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) )
35	6 8 34	sylancl	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) ≤ sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) )
36	7 27 28 29 30	ixxub	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐷 )
37	25 26 16 36	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐷 )
38	7 19 20 21 22	ixxub	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
39	11 12 18 38	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
40	35 37 39	3brtr3d	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ≤ 𝐵 )
41	33 40	jca	⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) )
42	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ* )
43	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ* )
44		simprl	⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐶 )
45		simprr	⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐷 ≤ 𝐵 )
46		ioossioo	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
47	42 43 44 45 46	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
48	41 47	impbida	⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) )