ordtri1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ordtri1		Structured version Visualization version GIF version

Theorem ordtri1 6339

Description: A trichotomy law for ordinals. (Contributed by NM, 25-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)

**Assertion**
Ref	Expression
ordtri1	⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

**Proof of Theorem ordtri1**
Step	Hyp	Ref	Expression
1		ordsseleq 6335	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
2		ordn2lp 6326	. . . . 5 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
3		imnan 399	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
4	2, 3	sylibr 234	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴))
5		ordirr 6324	. . . . 5 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
6		eleq2 2820	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
7	6	notbid 318	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
8	5, 7	syl5ibrcom 247	. . . 4 ⊢ (Ord 𝐵 → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
9	4, 8	jaao 956	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) → ¬ 𝐵 ∈ 𝐴))
10		ordtri3or 6338	. . . . . 6 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))
11		df-3or 1087	. . . . . 6 ⊢ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
12	10, 11	sylib 218	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ∨ 𝐵 ∈ 𝐴))
13	12	orcomd 871	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ∨ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
14	13	ord 864	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ 𝐵 ∈ 𝐴 → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
15	9, 14	impbid 212	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) ↔ ¬ 𝐵 ∈ 𝐴))
16	1, 15	bitrd 279	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 = wceq 1541 ∈ wcel 2111 ⊆ wss 3897 Ord word 6305

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-ext 2703 ax-sep 5232 ax-nul 5242 ax-pr 5368

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-ral 3048 df-rex 3057 df-rab 3396 df-v 3438 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5090 df-opab 5152 df-tr 5197 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-ord 6309

This theorem is referenced by: ontri1 6340 ordtri2 6341 ordtri4 6343 ordtr3 6352 ordintdif 6357 ordtri2or 6406 ordsucss 7748 ordsucsssuc 7753 ordsucuniel 7754 limsssuc 7780 ssnlim 7816 smoword 8286 tfrlem15 8311 nnaword 8542 nnawordex 8552 eldifsucnn 8579 nndomog 9122 onomeneq 9123 isfinite2 9182 unfilem1 9189 wofib 9431 cantnflem1 9579 ttrcltr 9606 dmttrcl 9611 alephgeom 9973 alephdom2 9978 cflim2 10154 fin67 10286 winainflem 10584 finminlem 36360 ordeldif 43299 ordeldifsucon 43300 ordeldif1o 43301

W3C validator