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

Metamath Proof Explorer

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