Theorem sotri 4978

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)

Hypotheses

Ref	Expression
soi.1	⊢ 𝑅 Or 𝑆
soi.2	⊢ 𝑅 ⊆ (𝑆 × 𝑆)

Assertion

Ref	Expression
sotri	⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Proof of Theorem sotri

Step	Hyp	Ref	Expression
1		soi.2	. . . . 5 ⊢ 𝑅 ⊆ (𝑆 × 𝑆)
2	1	brel 4635	. . . 4 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
3	2	simpld 111	. . 3 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ 𝑆)
4	1	brel 4635	. . 3 ⊢ (𝐵𝑅𝐶 → (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
5	3, 4	anim12i 336	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
6		soi.1	. . . 4 ⊢ 𝑅 Or 𝑆
7		sotr 4277	. . . 4 ⊢ ((𝑅 Or 𝑆 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
8	6, 7	mpan 421	. . 3 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
9	8	3expb 1186	. 2 ⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
10	5, 9	mpcom 36	1 ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963   ∈ wcel 2128   ⊆ wss 3102   class class class wbr 3965   Or wor 4254   × cxp 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4134  ax-pr 4168

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-br 3966  df-opab 4026  df-po 4255  df-iso 4256  df-xp 4589

This theorem is referenced by:  son2lpi  4979  ltsonq  7301  lt2addnq  7307  lt2mulnq  7308  ltbtwnnqq  7318  prarloclemarch2  7322  genplt2i  7413  addlocprlemgt  7437  nqprloc  7448  prmuloclemcalc  7468  ltsopr  7499  ltexprlemopl  7504  ltexprlemopu  7506  ltexprlemru  7515  prplnqu  7523  recexprlemlol  7529  recexprlemupu  7531  recexprlemdisj  7533  recexprlemss1l  7538  recexprlemss1u  7539  cauappcvgprlemopl  7549  cauappcvgprlemlol  7550  cauappcvgprlemupu  7552  cauappcvgprlemladdfu  7557  caucvgprlemk  7568  caucvgprlemnkj  7569  caucvgprlemnbj  7570  caucvgprlemm  7571  caucvgprlemopl  7572  caucvgprlemlol  7573  caucvgprlemupu  7575  caucvgprlemloc  7578  caucvgprlemladdfu  7580  caucvgprprlemk  7586  caucvgprprlemloccalc  7587  caucvgprprlemnkltj  7592  caucvgprprlemnkeqj  7593  caucvgprprlemnjltk  7594  caucvgprprlemnbj  7596  caucvgprprlemml  7597  caucvgprprlemopl  7600  caucvgprprlemlol  7601  caucvgprprlemupu  7603  lttrsr  7665  addgt0sr  7678  archsr  7685  caucvgsrlemcl  7692  caucvgsrlemfv  7694  suplocsrlemb  7709  suplocsrlempr  7710  suplocsrlem  7711  axpre-lttrn  7787