Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ontr2 | Structured version Visualization version GIF version |
Description: Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.) |
Ref | Expression |
---|---|
ontr2 | ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 6176 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | eloni 6176 | . 2 ⊢ (𝐶 ∈ On → Ord 𝐶) | |
3 | ordtr2 6210 | . 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) | |
4 | 1, 2, 3 | syl2an 599 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2113 ⊆ wss 3841 Ord word 6165 Oncon0 6166 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5164 ax-nul 5171 ax-pr 5293 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3399 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-pss 3860 df-nul 4210 df-if 4412 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-br 5028 df-opab 5090 df-tr 5134 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6169 df-on 6170 |
This theorem is referenced by: oeordsuc 8244 oelimcl 8250 oeeui 8252 omopthlem2 8307 omxpenlem 8660 oismo 9070 cantnflem1c 9216 cantnflem1 9218 cantnflem3 9220 rankr1ai 9293 rankxplim 9374 infxpenlem 9506 alephle 9581 pwcfsdom 10076 r1limwun 10229 onelssex 33226 onunel 33255 naddssim 33470 oldbdayim 33701 ontopbas 34247 ontgval 34250 |
Copyright terms: Public domain | W3C validator |