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 ↾ ℝ* ) )