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	syl6bbr	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 ) )
17	9 10 16	pm5.21nii	⊢ ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( < ∪ ( I ↾ ℝ* ) ) 𝑦 )
18	1 7 17	eqbrriv	⊢ ≤ = ( < ∪ ( I ↾ ℝ* ) )