Theorem ordtr1 4268

Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)

Assertion

Ref	Expression
ordtr1	⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Proof of Theorem ordtr1

Step	Hyp	Ref	Expression
1		ordtr 4258	. 2 ⊢ (Ord 𝐶 → Tr 𝐶)
2		trel 3991	. 2 ⊢ (Tr 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
3	1, 2	syl 14	1 ⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1461  Tr wtr 3984  Ord word 4242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-tru 1315  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-v 2657  df-in 3041  df-ss 3048  df-uni 3701  df-tr 3985  df-iord 4246

This theorem is referenced by:  ontr1  4269  ordwe  4448  dfsmo2  6136  smores2  6143  smoel  6149  tfr1onlemsucaccv  6190  tfr1onlembxssdm  6192  tfr1onlembfn  6193  tfr1onlemaccex  6197  tfr1onlemres  6198  tfrcllemsucaccv  6203  tfrcllembxssdm  6205  tfrcllembfn  6206  tfrcllemaccex  6210  tfrcllemres  6211  tfrcl  6213  ordiso2  6870