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

Metamath Proof Explorer

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 )