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

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 𝐴