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 ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
isso2i.2 ( ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
Assertion isso2i 𝑅 Or 𝐴

Proof

Step Hyp Ref Expression
1 isso2i.1 ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 ↔ ¬ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
2 isso2i.2 ( ( 𝑥𝐴𝑦𝐴𝑧𝐴 ) → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
3 equid 𝑥 = 𝑥
4 3 orci ( 𝑥 = 𝑥𝑥 𝑅 𝑥 )
5 nfv 𝑦 ( ( 𝑥𝐴𝑥𝐴 ) → ( ( 𝑥 = 𝑥𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
6 eleq1w ( 𝑦 = 𝑥 → ( 𝑦𝐴𝑥𝐴 ) )
7 6 anbi2d ( 𝑦 = 𝑥 → ( ( 𝑥𝐴𝑦𝐴 ) ↔ ( 𝑥𝐴𝑥𝐴 ) ) )
8 equequ2 ( 𝑦 = 𝑥 → ( 𝑥 = 𝑦𝑥 = 𝑥 ) )
9 breq1 ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑥𝑥 𝑅 𝑥 ) )
10 8 9 orbi12d ( 𝑦 = 𝑥 → ( ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑥 = 𝑥𝑥 𝑅 𝑥 ) ) )
11 breq2 ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦𝑥 𝑅 𝑥 ) )
12 11 notbid ( 𝑦 = 𝑥 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝑥 ) )
13 10 12 bibi12d ( 𝑦 = 𝑥 → ( ( ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) ↔ ( ( 𝑥 = 𝑥𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) ) )
14 7 13 imbi12d ( 𝑦 = 𝑥 → ( ( ( 𝑥𝐴𝑦𝐴 ) → ( ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) ) ↔ ( ( 𝑥𝐴𝑥𝐴 ) → ( ( 𝑥 = 𝑥𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) ) ) )
15 1 con2bid ( ( 𝑥𝐴𝑦𝐴 ) → ( ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑦 ) )
16 5 14 15 chvarfv ( ( 𝑥𝐴𝑥𝐴 ) → ( ( 𝑥 = 𝑥𝑥 𝑅 𝑥 ) ↔ ¬ 𝑥 𝑅 𝑥 ) )
17 4 16 mpbii ( ( 𝑥𝐴𝑥𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
18 17 anidms ( 𝑥𝐴 → ¬ 𝑥 𝑅 𝑥 )
19 15 biimprd ( ( 𝑥𝐴𝑦𝐴 ) → ( ¬ 𝑥 𝑅 𝑦 → ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
20 19 orrd ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
21 3orass ( ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦𝑦 𝑅 𝑥 ) ) )
22 20 21 sylibr ( ( 𝑥𝐴𝑦𝐴 ) → ( 𝑥 𝑅 𝑦𝑥 = 𝑦𝑦 𝑅 𝑥 ) )
23 18 2 22 issoi 𝑅 Or 𝐴