Metamath Proof Explorer

Theorem dfso2

Description: Quantifier-free definition of a strict order. (Contributed by Scott Fenton, 22-Feb-2013)

Ref Expression
Assertion dfso2 ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-so ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
2 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) )
3 brun ⊢ ( 𝑥 ( I ∪ ◡ 𝑅 ) 𝑦 ↔ ( 𝑥 I 𝑦 ∨ 𝑥 ◡ 𝑅 𝑦 ) )
4 vex ⊢ 𝑦 ∈ V
5 4 ideq ⊢ ( 𝑥 I 𝑦 ↔ 𝑥 = 𝑦 )
6 vex ⊢ 𝑥 ∈ V
7 6 4 brcnv ⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
8 5 7 orbi12i ⊢ ( ( 𝑥 I 𝑦 ∨ 𝑥 ◡ 𝑅 𝑦 ) ↔ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
9 3 8 bitr2i ⊢ ( ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ 𝑥 ( I ∪ ◡ 𝑅 ) 𝑦 )
10 9 orbi2i ⊢ ( ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑥 ( I ∪ ◡ 𝑅 ) 𝑦 ) )
11 3orass ⊢ ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑦 ∨ ( 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
12 brun ⊢ ( 𝑥 ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) 𝑦 ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑥 ( I ∪ ◡ 𝑅 ) 𝑦 ) )
13 10 11 12 3bitr4i ⊢ ( ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ 𝑥 ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) 𝑦 )
14 df-br ⊢ ( 𝑥 ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) )
15 13 14 bitr2i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ↔ ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
16 2 15 imbi12i ⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
17 16 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
18 relxp ⊢ Rel ( 𝐴 × 𝐴 )
19 ssrel ⊢ ( Rel ( 𝐴 × 𝐴 ) → ( ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) ) )
20 18 19 ax-mp ⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐴 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) )
21 r2al ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
22 17 20 21 3bitr4i ⊢ ( ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) )
23 22 anbi2i ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) ↔ ( 𝑅 Po 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 𝑅 𝑥 ) ) )
24 1 23 bitr4i ⊢ ( 𝑅 Or 𝐴 ↔ ( 𝑅 Po 𝐴 ∧ ( 𝐴 × 𝐴 ) ⊆ ( 𝑅 ∪ ( I ∪ ◡ 𝑅 ) ) ) )