Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ordsucss | Structured version Visualization version GIF version |
Description: The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998.) |
Ref | Expression |
---|---|
ordsucss | ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordelord 6235 | . . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴) | |
2 | ordnbtwn 6303 | . . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | |
3 | imnan 403 | . . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | |
4 | 2, 3 | sylibr 237 | . . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴)) |
5 | 4 | adantr 484 | . . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴)) |
6 | ordsuc 7593 | . . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | |
7 | ordtri1 6246 | . . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) | |
8 | 6, 7 | sylanb 584 | . . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) |
9 | 5, 8 | sylibrd 262 | . . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
10 | 1, 9 | sylan 583 | . . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
11 | 10 | exp31 423 | . . 3 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)))) |
12 | 11 | pm2.43b 55 | . 2 ⊢ (𝐴 ∈ 𝐵 → (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵))) |
13 | 12 | pm2.43b 55 | 1 ⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∈ wcel 2110 ⊆ wss 3866 Ord word 6212 suc csuc 6215 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-11 2158 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 ax-un 7523 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3or 1090 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-pss 3885 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-tp 4546 df-op 4548 df-uni 4820 df-br 5054 df-opab 5116 df-tr 5162 df-eprel 5460 df-po 5468 df-so 5469 df-fr 5509 df-we 5511 df-ord 6216 df-on 6217 df-suc 6219 |
This theorem is referenced by: ordelsuc 7599 ordsucelsuc 7601 orduniorsuc 7609 tfindsg2 7640 oaordi 8274 oawordeulem 8282 omeulem2 8311 oeworde 8321 oelimcl 8328 oeeui 8330 nnaordi 8346 nnawordex 8365 oaabs2 8374 omxpenlem 8746 inf3lem5 9247 cantnflt 9287 cantnflem1d 9303 cnfcom 9315 r1ordg 9394 rankr1ag 9418 cfslb2n 9882 cfsmolem 9884 fin23lem26 9939 isf32lem3 9969 ttukeylem7 10129 indpi 10521 nolesgn2ores 33612 nogesgn1ores 33614 nosupbday 33645 nosupres 33647 nosupbnd1lem1 33648 nosupbnd2 33656 noinfbday 33660 noinfres 33662 noinfbnd1lem1 33663 noinfbnd2 33671 |
Copyright terms: Public domain | W3C validator |