Metamath Proof Explorer

Theorem isso2i

Description: Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996) (Revised by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypotheses isso2i.1 
|- ( ( x e. A /\ y e. A ) -> ( x R y <-> -. ( x = y \/ y R x ) ) )
isso2i.2 
|- ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )
Assertion isso2i 
|- R Or A

Proof

Step Hyp Ref Expression
1 isso2i.1 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y <-> -. ( x = y \/ y R x ) ) )
2 isso2i.2 
 |-  ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R y /\ y R z ) -> x R z ) )
3 equid 
 |-  x = x
4 3 orci 
 |-  ( x = x \/ x R x )
5 nfv 
 |-  F/ y ( ( x e. A /\ x e. A ) -> ( ( x = x \/ x R x ) <-> -. x R x ) )
6 eleq1w 
 |-  ( y = x -> ( y e. A <-> x e. A ) )
7 6 anbi2d 
 |-  ( y = x -> ( ( x e. A /\ y e. A ) <-> ( x e. A /\ x e. A ) ) )
8 equequ2 
 |-  ( y = x -> ( x = y <-> x = x ) )
9 breq1 
 |-  ( y = x -> ( y R x <-> x R x ) )
10 8 9 orbi12d 
 |-  ( y = x -> ( ( x = y \/ y R x ) <-> ( x = x \/ x R x ) ) )
11 breq2 
 |-  ( y = x -> ( x R y <-> x R x ) )
12 11 notbid 
 |-  ( y = x -> ( -. x R y <-> -. x R x ) )
13 10 12 bibi12d 
 |-  ( y = x -> ( ( ( x = y \/ y R x ) <-> -. x R y ) <-> ( ( x = x \/ x R x ) <-> -. x R x ) ) )
14 7 13 imbi12d 
 |-  ( y = x -> ( ( ( x e. A /\ y e. A ) -> ( ( x = y \/ y R x ) <-> -. x R y ) ) <-> ( ( x e. A /\ x e. A ) -> ( ( x = x \/ x R x ) <-> -. x R x ) ) ) )
15 1 con2bid 
 |-  ( ( x e. A /\ y e. A ) -> ( ( x = y \/ y R x ) <-> -. x R y ) )
16 5 14 15 chvarfv 
 |-  ( ( x e. A /\ x e. A ) -> ( ( x = x \/ x R x ) <-> -. x R x ) )
17 4 16 mpbii 
 |-  ( ( x e. A /\ x e. A ) -> -. x R x )
18 17 anidms 
 |-  ( x e. A -> -. x R x )
19 15 biimprd 
 |-  ( ( x e. A /\ y e. A ) -> ( -. x R y -> ( x = y \/ y R x ) ) )
20 19 orrd 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y \/ ( x = y \/ y R x ) ) )
21 3orass 
 |-  ( ( x R y \/ x = y \/ y R x ) <-> ( x R y \/ ( x = y \/ y R x ) ) )
22 20 21 sylibr 
 |-  ( ( x e. A /\ y e. A ) -> ( x R y \/ x = y \/ y R x ) )
23 18 2 22 issoi 
 |-  R Or A