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

Metamath Proof Explorer

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