Metamath Proof Explorer


Theorem leordtvallem2

Description: Lemma for leordtval . (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses leordtval.1 A = ran x * x +∞
leordtval.2 B = ran x * −∞ x
Assertion leordtvallem2 B = ran x * y * | ¬ x y

Proof

Step Hyp Ref Expression
1 leordtval.1 A = ran x * x +∞
2 leordtval.2 B = ran x * −∞ x
3 icossxr −∞ x *
4 sseqin2 −∞ x * * −∞ x = −∞ x
5 3 4 mpbi * −∞ x = −∞ x
6 mnfxr −∞ *
7 simpl x * y * x *
8 elico1 −∞ * x * y −∞ x y * −∞ y y < x
9 6 7 8 sylancr x * y * y −∞ x y * −∞ y y < x
10 simpr x * y * y *
11 mnfle y * −∞ y
12 10 11 jccir x * y * y * −∞ y
13 12 biantrurd x * y * y < x y * −∞ y y < x
14 df-3an y * −∞ y y < x y * −∞ y y < x
15 13 14 bitr4di x * y * y < x y * −∞ y y < x
16 xrltnle y * x * y < x ¬ x y
17 16 ancoms x * y * y < x ¬ x y
18 9 15 17 3bitr2d x * y * y −∞ x ¬ x y
19 18 rabbi2dva x * * −∞ x = y * | ¬ x y
20 5 19 eqtr3id x * −∞ x = y * | ¬ x y
21 20 mpteq2ia x * −∞ x = x * y * | ¬ x y
22 21 rneqi ran x * −∞ x = ran x * y * | ¬ x y
23 2 22 eqtri B = ran x * y * | ¬ x y