Theorem cnvso

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

	Ref	Expression
Assertion	cnvso	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cnvpo	⊢ ( 𝑅 Po 𝐴 ↔ ◡ 𝑅 Po 𝐴 )
2		ralcom	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
3		vex	⊢ 𝑦 ∈ V
4		vex	⊢ 𝑥 ∈ V
5	3 4	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
6		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
7	4 3	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
8	5 6 7	3orbi123i	⊢ ( ( 𝑦 ◡ 𝑅 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ◡ 𝑅 𝑦 ) ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
9	8	2ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ◡ 𝑅 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
10	2 9	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ◡ 𝑅 𝑦 ) )
11	1 10	anbi12i	⊢ ( ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ↔ ( ◡ 𝑅 Po 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ◡ 𝑅 𝑦 ) ) )
12		df-so	⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
13		df-so	⊢ ( ◡ 𝑅 Or 𝐴 ↔ ( ◡ 𝑅 Po 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑥 ∈ 𝐴 ( 𝑦 ◡ 𝑅 𝑥 ∨ 𝑦 = 𝑥 ∨ 𝑥 ◡ 𝑅 𝑦 ) ) )
14	11 12 13	3bitr4i	⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )