Theorem dflt2

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

	Ref	Expression
Assertion	dflt2	⊢ < = ( ≤ ∖ I )

Proof

Step	Hyp	Ref	Expression
1		ltrel	⊢ Rel <
2		difss	⊢ ( ≤ ∖ I ) ⊆ ≤
3		lerel	⊢ Rel ≤
4		relss	⊢ ( ( ≤ ∖ I ) ⊆ ≤ → ( Rel ≤ → Rel ( ≤ ∖ I ) ) )
5	2 3 4	mp2	⊢ Rel ( ≤ ∖ I )
6		ltrelxr	⊢ < ⊆ ( ℝ* × ℝ* )
7	6	brel	⊢ ( 𝑥 < 𝑦 → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
8		lerelxr	⊢ ≤ ⊆ ( ℝ* × ℝ* )
9	2 8	sstri	⊢ ( ≤ ∖ I ) ⊆ ( ℝ* × ℝ* )
10	9	brel	⊢ ( 𝑥 ( ≤ ∖ I ) 𝑦 → ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) )
11		xrltlen	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥 ) ) )
12		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
13		vex	⊢ 𝑦 ∈ V
14	13	ideq	⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
15	12 14	bitr4i	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 I 𝑦 )
16	15	necon3abii	⊢ ( 𝑦 ≠ 𝑥 ↔ ¬ 𝑥 I 𝑦 )
17	16	anbi2i	⊢ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≠ 𝑥 ) ↔ ( 𝑥 ≤ 𝑦 ∧ ¬ 𝑥 I 𝑦 ) )
18	11 17	bitrdi	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ ¬ 𝑥 I 𝑦 ) ) )
19		brdif	⊢ ( 𝑥 ( ≤ ∖ I ) 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ ¬ 𝑥 I 𝑦 ) )
20	18 19	bitr4di	⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 < 𝑦 ↔ 𝑥 ( ≤ ∖ I ) 𝑦 ) )
21	7 10 20	pm5.21nii	⊢ ( 𝑥 < 𝑦 ↔ 𝑥 ( ≤ ∖ I ) 𝑦 )
22	1 5 21	eqbrriv	⊢ < = ( ≤ ∖ I )