This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfle2

Description: Alternative definition of 'less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 6-Nov-2015)

Ref Expression
Assertion dfle2 ≤ = ( < ∪ ( I ↾ ℝ* ) )

Proof

Step Hyp Ref Expression
1 lerel ⊢ Rel ≤
2 ltrelxr ⊢ < ⊆ ( ℝ* × ℝ* )
3 idssxp ⊢ ( I ↾ ℝ* ) ⊆ ( ℝ* × ℝ* )
4 2 3 unssi ⊢ ( < ∪ ( I ↾ ℝ* ) ) ⊆ ( ℝ* × ℝ* )
5 relxp ⊢ Rel ( ℝ* × ℝ* )
6 relss ⊢ ( ( < ∪ ( I ↾ ℝ* ) ) ⊆ ( ℝ* × ℝ* ) → ( Rel ( ℝ* × ℝ* ) → Rel ( < ∪ ( I ↾ ℝ* ) ) ) )
7 4 5 6 mp2 ⊢ Rel ( < ∪ ( I ↾ ℝ* ) )
8 lerelxr ⊢ ≤ ⊆ ( ℝ* × ℝ* )
9 8 brel ⊢ ( 𝑥 ≤ 𝑦 → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
10 4 brel ⊢ ( 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
11 xrleloe ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
12 resieq ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ( I ↾ ℝ* ) 𝑦 ↔ 𝑥 = 𝑦 ) )
13 12 orbi2d ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( ( 𝑥 < 𝑦 ∨ 𝑥 ( I ↾ ℝ* ) 𝑦 ) ↔ ( 𝑥 < 𝑦 ∨ 𝑥 = 𝑦 ) ) )
14 11 13 bitr4d ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 ( I ↾ ℝ* ) 𝑦 ) ) )
15 brun ⊢ ( 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑥 ( I ↾ ℝ* ) 𝑦 ) )
16 14 15 bitr4di ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 ) )
17 9 10 16 pm5.21nii ⊢ ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 )
18 1 7 17 eqbrriv ⊢ ≤ = ( < ∪ ( I ↾ ℝ* ) )