![]() |
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 6091 | . . . . 5 ⊢ ((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) → Ord 𝐴) | |
2 | ordnbtwn 6159 | . . . . . . . 8 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | |
3 | imnan 400 | . . . . . . . 8 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴)) | |
4 | 2, 3 | sylibr 235 | . . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴)) |
5 | 4 | adantr 481 | . . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝐴)) |
6 | ordsuc 7388 | . . . . . . 7 ⊢ (Ord 𝐴 ↔ Ord suc 𝐴) | |
7 | ordtri1 6102 | . . . . . . 7 ⊢ ((Ord suc 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) | |
8 | 6, 7 | sylanb 581 | . . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (suc 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ suc 𝐴)) |
9 | 5, 8 | sylibrd 260 | . . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
10 | 1, 9 | sylan 580 | . . . 4 ⊢ (((Ord 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 → suc 𝐴 ⊆ 𝐵)) |
11 | 10 | exp31 420 | . . 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 207 ∧ wa 396 ∈ wcel 2080 ⊆ wss 3861 Ord word 6068 suc csuc 6071 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pr 5224 ax-un 7322 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-sbc 3708 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-pss 3878 df-nul 4214 df-if 4384 df-sn 4475 df-pr 4477 df-tp 4479 df-op 4481 df-uni 4748 df-br 4965 df-opab 5027 df-tr 5067 df-eprel 5356 df-po 5365 df-so 5366 df-fr 5405 df-we 5407 df-ord 6072 df-on 6073 df-suc 6075 |
This theorem is referenced by: ordelsuc 7394 ordsucelsuc 7396 orduniorsuc 7404 tfindsg2 7435 oaordi 8025 oawordeulem 8033 omeulem2 8062 oeworde 8072 oelimcl 8079 oeeui 8081 nnaordi 8097 nnawordex 8116 oaabs2 8125 omxpenlem 8468 inf3lem5 8944 cantnflt 8984 cantnflem1d 9000 cnfcom 9012 r1ordg 9056 rankr1ag 9080 cfslb2n 9539 cfsmolem 9541 fin23lem26 9596 isf32lem3 9626 ttukeylem7 9786 indpi 10178 nolesgn2ores 32782 nosupres 32810 nosupbnd1lem1 32811 nosupbnd2 32819 |
Copyright terms: Public domain | W3C validator |