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

Metamath Proof Explorer

Theorem swopo

Description: A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypotheses swopo.1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) )
swopo.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) ) )
Assertion swopo ( 𝜑 → 𝑅 Po 𝐴 )

Proof

Step Hyp Ref Expression
1 swopo.1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) )
2 swopo.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑥 𝑅 𝑦 → ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) ) )
3 id ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴 )
4 3 ancli ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) )
5 1 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) )
6 breq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
7 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 𝑥 ) )
8 7 notbid ⊢ ( 𝑦 = 𝑥 → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑅 𝑥 ) )
9 6 8 imbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑥 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑥 ) ) )
10 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 𝑅 𝑧 ↔ 𝑥 𝑅 𝑥 ) )
11 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
12 11 notbid ⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑥 ) )
13 10 12 imbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑥 → ¬ 𝑥 𝑅 𝑥 ) ) )
14 9 13 rspc2va ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) ) → ( 𝑥 𝑅 𝑥 → ¬ 𝑥 𝑅 𝑥 ) )
15 4 5 14 syl2anr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑥 → ¬ 𝑥 𝑅 𝑥 ) )
16 15 pm2.01d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝑥 𝑅 𝑥 )
17 1 3adantr1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑦 𝑅 𝑧 → ¬ 𝑧 𝑅 𝑦 ) )
18 2 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( 𝑥 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) )
19 18 orcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( 𝑧 𝑅 𝑦 ∨ 𝑥 𝑅 𝑧 ) )
20 19 ord ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ 𝑥 𝑅 𝑦 ) → ( ¬ 𝑧 𝑅 𝑦 → 𝑥 𝑅 𝑧 ) )
21 20 expimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑦 ∧ ¬ 𝑧 𝑅 𝑦 ) → 𝑥 𝑅 𝑧 ) )
22 17 21 sylan2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
23 16 22 ispod ⊢ ( 𝜑 → 𝑅 Po 𝐴 )