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 6368

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 6364	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵)))
2		ordn2lp 6355	. . . . 5 ⊢ (Ord 𝐴 → ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
3		imnan 399	. . . . 5 ⊢ ((𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴) ↔ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐴))
4	2, 3	sylibr 234	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ 𝐵 → ¬ 𝐵 ∈ 𝐴))
5		ordirr 6353	. . . . 5 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
6		eleq2 2818	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
7	6	notbid 318	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
8	5, 7	syl5ibrcom 247	. . . 4 ⊢ (Ord 𝐵 → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
9	4, 8	jaao 956	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵) → ¬ 𝐵 ∈ 𝐴))
10		ordtri3or 6367	. . . . . 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 1540 ∈ wcel 2109 ⊆ wss 3917 Ord word 6334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-ext 2702 ax-sep 5254 ax-nul 5264 ax-pr 5390

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2066 df-clab 2709 df-cleq 2722 df-clel 2804 df-ne 2927 df-ral 3046 df-rex 3055 df-rab 3409 df-v 3452 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-br 5111 df-opab 5173 df-tr 5218 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-ord 6338

This theorem is referenced by: ontri1 6369 ordtri2 6370 ordtri4 6372 ordtr3 6381 ordintdif 6386 ordtri2or 6435 ordsucss 7796 ordsucsssuc 7801 ordsucuniel 7802 limsssuc 7829 ssnlim 7865 smoword 8338 tfrlem15 8363 nnaword 8594 nnawordex 8604 eldifsucnn 8631 nndomog 9183 onomeneq 9184 isfinite2 9252 unfilem1 9261 wofib 9505 cantnflem1 9649 ttrcltr 9676 dmttrcl 9681 alephgeom 10042 alephdom2 10047 cflim2 10223 fin67 10355 winainflem 10653 finminlem 36313 ordeldif 43254 ordeldifsucon 43255 ordeldif1o 43256

W3C validator