ioorf

Description: Define a function from open intervals to their endpoints. (Contributed by Mario Carneiro, 26-Mar-2015) (Revised by AV, 13-Sep-2020)

		Ref	Expression
	Hypothesis	ioorf.1	⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) )
	Assertion	ioorf	⊢ 𝐹 : ran (,) ⟶ ( ≤ ∩ ( ℝ^* × ℝ^* ) )

Proof

Step	Hyp	Ref	Expression
1		ioorf.1	⊢ 𝐹 = ( 𝑥 ∈ ran (,) ↦ if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) )
2		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
3		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
4		ovelrn	⊢ ( (,) Fn ( ℝ^* × ℝ^* ) → ( 𝑥 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ^* ∃ 𝑏 ∈ ℝ^* 𝑥 = ( 𝑎 (,) 𝑏 ) ) )
5	2 3 4	mp2b	⊢ ( 𝑥 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ^* ∃ 𝑏 ∈ ℝ^* 𝑥 = ( 𝑎 (,) 𝑏 ) )
6		0le0	⊢ 0 ≤ 0
7		df-br	⊢ ( 0 ≤ 0 ↔ ⟨ 0 , 0 ⟩ ∈ ≤ )
8	6 7	mpbi	⊢ ⟨ 0 , 0 ⟩ ∈ ≤
9		0xr	⊢ 0 ∈ ℝ^*
10		opelxpi	⊢ ( ( 0 ∈ ℝ^* ∧ 0 ∈ ℝ^* ) → ⟨ 0 , 0 ⟩ ∈ ( ℝ^* × ℝ^* ) )
11	9 9 10	mp2an	⊢ ⟨ 0 , 0 ⟩ ∈ ( ℝ^* × ℝ^* )
12	8 11	elini	⊢ ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) )
13	12	a1i	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ 𝑥 = ∅ ) → ⟨ 0 , 0 ⟩ ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
14		simplr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 = ( 𝑎 (,) 𝑏 ) )
15	14	infeq1d	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( 𝑥 , ℝ^* , < ) = inf ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) )
16		simplll	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎 ∈ ℝ^* )
17		simpllr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑏 ∈ ℝ^* )
18		simpr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ¬ 𝑥 = ∅ )
19	18	neqned	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑥 ≠ ∅ )
20	14 19	eqnetrrd	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑎 (,) 𝑏 ) ≠ ∅ )
21		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
22		idd	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( 𝑤 < 𝑏 → 𝑤 < 𝑏 ) )
23		xrltle	⊢ ( ( 𝑤 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( 𝑤 < 𝑏 → 𝑤 ≤ 𝑏 ) )
24		idd	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝑎 < 𝑤 → 𝑎 < 𝑤 ) )
25		xrltle	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑤 ∈ ℝ^* ) → ( 𝑎 < 𝑤 → 𝑎 ≤ 𝑤 ) )
26	21 22 23 24 25	ixxlb	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → inf ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) = 𝑎 )
27	16 17 20 26	syl3anc	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) = 𝑎 )
28	15 27	eqtrd	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → inf ( 𝑥 , ℝ^* , < ) = 𝑎 )
29	14	supeq1d	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( 𝑥 , ℝ^* , < ) = sup ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) )
30	21 22 23 24 25	ixxub	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ∧ ( 𝑎 (,) 𝑏 ) ≠ ∅ ) → sup ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) = 𝑏 )
31	16 17 20 30	syl3anc	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( ( 𝑎 (,) 𝑏 ) , ℝ^* , < ) = 𝑏 )
32	29 31	eqtrd	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → sup ( 𝑥 , ℝ^* , < ) = 𝑏 )
33	28 32	opeq12d	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ = ⟨ 𝑎 , 𝑏 ⟩ )
34		ioon0	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
35	34	ad2antrr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( ( 𝑎 (,) 𝑏 ) ≠ ∅ ↔ 𝑎 < 𝑏 ) )
36	20 35	mpbid	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎 < 𝑏 )
37		xrltle	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( 𝑎 < 𝑏 → 𝑎 ≤ 𝑏 ) )
38	37	ad2antrr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ( 𝑎 < 𝑏 → 𝑎 ≤ 𝑏 ) )
39	36 38	mpd	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → 𝑎 ≤ 𝑏 )
40		df-br	⊢ ( 𝑎 ≤ 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ≤ )
41	39 40	sylib	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ≤ )
42		opelxpi	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ^* × ℝ^* ) )
43	42	ad2antrr	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ℝ^* × ℝ^* ) )
44	41 43	elind	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ 𝑎 , 𝑏 ⟩ ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
45	33 44	eqeltrd	⊢ ( ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) ∧ ¬ 𝑥 = ∅ ) → ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
46	13 45	ifclda	⊢ ( ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) ∧ 𝑥 = ( 𝑎 (,) 𝑏 ) ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
47	46	ex	⊢ ( ( 𝑎 ∈ ℝ^* ∧ 𝑏 ∈ ℝ^* ) → ( 𝑥 = ( 𝑎 (,) 𝑏 ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) ) )
48	47	rexlimivv	⊢ ( ∃ 𝑎 ∈ ℝ^* ∃ 𝑏 ∈ ℝ^* 𝑥 = ( 𝑎 (,) 𝑏 ) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
49	5 48	sylbi	⊢ ( 𝑥 ∈ ran (,) → if ( 𝑥 = ∅ , ⟨ 0 , 0 ⟩ , ⟨ inf ( 𝑥 , ℝ^* , < ) , sup ( 𝑥 , ℝ^* , < ) ⟩ ) ∈ ( ≤ ∩ ( ℝ^* × ℝ^* ) ) )
50	1 49	fmpti	⊢ 𝐹 : ran (,) ⟶ ( ≤ ∩ ( ℝ^* × ℝ^* ) )

Metamath Proof Explorer

Theorem ioorf

Proof