Metamath Proof Explorer

Theorem sotri3

Description: A transitivity relation. (Read A < B and B <_ C implies A < C .) (Contributed by Mario Carneiro, 10-May-2013)

Ref Expression
Hypotheses soi.1 ⊢ R Or S
soi.2 ⊢ R ⊆ S × S
Assertion sotri3 ⊢ C ∈ S ∧ A R B ∧ ¬ C R B → A R C

Proof

Step Hyp Ref Expression
1 soi.1 ⊢ R Or S
2 soi.2 ⊢ R ⊆ S × S
3 2 brel ⊢ A R B → A ∈ S ∧ B ∈ S
4 3 simprd ⊢ A R B → B ∈ S
5 sotric ⊢ R Or S ∧ C ∈ S ∧ B ∈ S → C R B ↔ ¬ C = B ∨ B R C
6 1 5 mpan ⊢ C ∈ S ∧ B ∈ S → C R B ↔ ¬ C = B ∨ B R C
7 6 con2bid ⊢ C ∈ S ∧ B ∈ S → C = B ∨ B R C ↔ ¬ C R B
8 breq2 ⊢ C = B → A R C ↔ A R B
9 8 biimprd ⊢ C = B → A R B → A R C
10 1 2 sotri ⊢ A R B ∧ B R C → A R C
11 10 expcom ⊢ B R C → A R B → A R C
12 9 11 jaoi ⊢ C = B ∨ B R C → A R B → A R C
13 7 12 syl6bir ⊢ C ∈ S ∧ B ∈ S → ¬ C R B → A R B → A R C
14 13 com3r ⊢ A R B → C ∈ S ∧ B ∈ S → ¬ C R B → A R C
15 4 14 mpan2d ⊢ A R B → C ∈ S → ¬ C R B → A R C
16 15 3imp21 ⊢ C ∈ S ∧ A R B ∧ ¬ C R B → A R C