Theorem sotri 5132

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 4778	. . . 4 ⊢ (𝐴𝑅𝐵 → (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆))
3	2	simpld 112	. . 3 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ 𝑆)
4	1	brel 4778	. . 3 ⊢ (𝐵𝑅𝐶 → (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆))
5	3, 4	anim12i 338	. 2 ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → (𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)))
6		soi.1	. . . 4 ⊢ 𝑅 Or 𝑆
7		sotr 4415	. . . 4 ⊢ ((𝑅 Or 𝑆 ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
8	6, 7	mpan 424	. . 3 ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
9	8	3expb 1230	. 2 ⊢ ((𝐴 ∈ 𝑆 ∧ (𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆)) → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶))
10	5, 9	mpcom 36	1 ⊢ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004   ∈ wcel 2202   ⊆ wss 3200   class class class wbr 4088   Or wor 4392   × cxp 4723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-po 4393  df-iso 4394  df-xp 4731

This theorem is referenced by:  son2lpi  5133  ltsonq  7617  lt2addnq  7623  lt2mulnq  7624  ltbtwnnqq  7634  prarloclemarch2  7638  genplt2i  7729  addlocprlemgt  7753  nqprloc  7764  prmuloclemcalc  7784  ltsopr  7815  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemru  7831  prplnqu  7839  recexprlemlol  7845  recexprlemupu  7847  recexprlemdisj  7849  recexprlemss1l  7854  recexprlemss1u  7855  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemupu  7868  cauappcvgprlemladdfu  7873  caucvgprlemk  7884  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemupu  7891  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprprlemk  7902  caucvgprprlemloccalc  7903  caucvgprprlemnkltj  7908  caucvgprprlemnkeqj  7909  caucvgprprlemnjltk  7910  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemupu  7919  lttrsr  7981  addgt0sr  7994  archsr  8001  caucvgsrlemcl  8008  caucvgsrlemfv  8010  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axpre-lttrn  8103