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 𝐴 )