Metamath Proof Explorer

Theorem qextlt

Description: An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion qextlt ⊢A∈ℝ*∧B∈ℝ*→A=B↔∀x∈ℚx<A↔x<B

Proof

Step Hyp Ref Expression
1 breq2 ⊢A=B→x<A↔x<B
2 1 ralrimivw ⊢A=B→∀x∈ℚx<A↔x<B
3 xrlttri2 ⊢A∈ℝ*∧B∈ℝ*→A≠B↔A<B∨B<A
4 qextltlem ⊢A∈ℝ*∧B∈ℝ*→A<B→∃x∈ℚ¬x<A↔x<B∧¬x≤A↔x≤B
5 simpl ⊢¬x<A↔x<B∧¬x≤A↔x≤B→¬x<A↔x<B
6 5 reximi ⊢∃x∈ℚ¬x<A↔x<B∧¬x≤A↔x≤B→∃x∈ℚ¬x<A↔x<B
7 4 6 syl6 ⊢A∈ℝ*∧B∈ℝ*→A<B→∃x∈ℚ¬x<A↔x<B
8 qextltlem ⊢B∈ℝ*∧A∈ℝ*→B<A→∃x∈ℚ¬x<B↔x<A∧¬x≤B↔x≤A
9 simpl ⊢¬x<B↔x<A∧¬x≤B↔x≤A→¬x<B↔x<A
10 bicom ⊢x<B↔x<A↔x<A↔x<B
11 9 10 sylnib ⊢¬x<B↔x<A∧¬x≤B↔x≤A→¬x<A↔x<B
12 11 reximi ⊢∃x∈ℚ¬x<B↔x<A∧¬x≤B↔x≤A→∃x∈ℚ¬x<A↔x<B
13 8 12 syl6 ⊢B∈ℝ*∧A∈ℝ*→B<A→∃x∈ℚ¬x<A↔x<B
14 13 ancoms ⊢A∈ℝ*∧B∈ℝ*→B<A→∃x∈ℚ¬x<A↔x<B
15 7 14 jaod ⊢A∈ℝ*∧B∈ℝ*→A<B∨B<A→∃x∈ℚ¬x<A↔x<B
16 3 15 sylbid ⊢A∈ℝ*∧B∈ℝ*→A≠B→∃x∈ℚ¬x<A↔x<B
17 rexnal ⊢∃x∈ℚ¬x<A↔x<B↔¬∀x∈ℚx<A↔x<B
18 16 17 imbitrdi ⊢A∈ℝ*∧B∈ℝ*→A≠B→¬∀x∈ℚx<A↔x<B
19 18 necon4ad ⊢A∈ℝ*∧B∈ℝ*→∀x∈ℚx<A↔x<B→A=B
20 2 19 impbid2 ⊢A∈ℝ*∧B∈ℝ*→A=B↔∀x∈ℚx<A↔x<B