Theorem cnvpo

Description: The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005)

	Ref	Expression
Assertion	cnvpo	⊢ ( 𝑅 Po 𝐴 ↔ ◡ 𝑅 Po 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		r19.26	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) ↔ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
2		vex	⊢ 𝑧 ∈ V
3	2 2	brcnv	⊢ ( 𝑧 ◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑧 )
4		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
5	4 4	breq12d	⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝑅 𝑧 ↔ 𝑥 𝑅 𝑥 ) )
6	3 5	bitrid	⊢ ( 𝑧 = 𝑥 → ( 𝑧 ◡ 𝑅 𝑧 ↔ 𝑥 𝑅 𝑥 ) )
7	6	notbid	⊢ ( 𝑧 = 𝑥 → ( ¬ 𝑧 ◡ 𝑅 𝑧 ↔ ¬ 𝑥 𝑅 𝑥 ) )
8	7	cbvralvw	⊢ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ◡ 𝑅 𝑧 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
9		vex	⊢ 𝑦 ∈ V
10	2 9	brcnv	⊢ ( 𝑧 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑧 )
11		vex	⊢ 𝑥 ∈ V
12	9 11	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
13	10 12	anbi12ci	⊢ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) )
14	2 11	brcnv	⊢ ( 𝑧 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑧 )
15	13 14	imbi12i	⊢ ( ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ↔ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
16	15	ralbii	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) )
17	8 16	anbi12i	⊢ ( ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
18	1 17	bitr2i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
19	18	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
20		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
21		ralidm	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
22		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
23		rzal	⊢ ( 𝐴 = ∅ → ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
24	22 23	2thd	⊢ ( 𝐴 = ∅ → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )
25		r19.3rzv	⊢ ( 𝐴 ≠ ∅ → ( ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )
26	25	ralbidv	⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ) )
27	24 26	pm2.61ine	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
28	21 27	bitr2i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 )
29	28	anbi1i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
30	20 29	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
31		r19.26	⊢ ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
32	31	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
33		r19.26	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
34	30 32 33	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 𝑅 𝑥 ∧ ∀ 𝑧 ∈ 𝐴 ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
35		ralcom	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
36	19 34 35	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
37	36	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
38		ralcom	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
39		ralcom	⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
40	37 38 39	3bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
41		df-po	⊢ ( 𝑅 Po 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑥 𝑅 𝑥 ∧ ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → 𝑥 𝑅 𝑧 ) ) )
42		df-po	⊢ ( ◡ 𝑅 Po 𝐴 ↔ ∀ 𝑧 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( ¬ 𝑧 ◡ 𝑅 𝑧 ∧ ( ( 𝑧 ◡ 𝑅 𝑦 ∧ 𝑦 ◡ 𝑅 𝑥 ) → 𝑧 ◡ 𝑅 𝑥 ) ) )
43	40 41 42	3bitr4i	⊢ ( 𝑅 Po 𝐴 ↔ ◡ 𝑅 Po 𝐴 )