![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orddisj | Structured version Visualization version GIF version |
Description: An ordinal class and its singleton are disjoint. (Contributed by NM, 19-May-1998.) |
Ref | Expression |
---|---|
orddisj | ⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordirr 6387 | . 2 ⊢ (Ord 𝐴 → ¬ 𝐴 ∈ 𝐴) | |
2 | disjsn 4716 | . 2 ⊢ ((𝐴 ∩ {𝐴}) = ∅ ↔ ¬ 𝐴 ∈ 𝐴) | |
3 | 1, 2 | sylibr 233 | 1 ⊢ (Ord 𝐴 → (𝐴 ∩ {𝐴}) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1534 ∈ wcel 2099 ∩ cin 3946 ∅c0 4323 {csn 4629 Ord word 6368 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-br 5149 df-opab 5211 df-eprel 5582 df-fr 5633 df-we 5635 df-ord 6372 |
This theorem is referenced by: orddif 6465 omsucne 7889 tfrlem10 8408 enrefnn 9072 pssnn 9193 unfi 9197 phplem2OLD 9243 isinf 9285 isinfOLD 9286 pssnnOLD 9290 dif1ennnALT 9302 ackbij1lem5 10248 ackbij1lem14 10257 ackbij1lem16 10259 unsnen 10577 pwfi2f1o 42520 |
Copyright terms: Public domain | W3C validator |