Theorem sotri 5025

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 978   ∈ wcel 2148   ⊆ wss 3130   class class class wbr 4004   Or wor 4296   × cxp 4625

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-pow 4175  ax-pr 4210

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2740  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005  df-opab 4066  df-po 4297  df-iso 4298  df-xp 4633

This theorem is referenced by:  son2lpi  5026  ltsonq  7397  lt2addnq  7403  lt2mulnq  7404  ltbtwnnqq  7414  prarloclemarch2  7418  genplt2i  7509  addlocprlemgt  7533  nqprloc  7544  prmuloclemcalc  7564  ltsopr  7595  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemru  7611  prplnqu  7619  recexprlemlol  7625  recexprlemupu  7627  recexprlemdisj  7629  recexprlemss1l  7634  recexprlemss1u  7635  cauappcvgprlemopl  7645  cauappcvgprlemlol  7646  cauappcvgprlemupu  7648  cauappcvgprlemladdfu  7653  caucvgprlemk  7664  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemupu  7671  caucvgprlemloc  7674  caucvgprlemladdfu  7676  caucvgprprlemk  7682  caucvgprprlemloccalc  7683  caucvgprprlemnkltj  7688  caucvgprprlemnkeqj  7689  caucvgprprlemnjltk  7690  caucvgprprlemnbj  7692  caucvgprprlemml  7693  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemupu  7699  lttrsr  7761  addgt0sr  7774  archsr  7781  caucvgsrlemcl  7788  caucvgsrlemfv  7790  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axpre-lttrn  7883