ordtri3 - Metamath Proof Explorer

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

Theorem ordtri3 6353

Description: A trichotomy law for ordinals. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by JJ, 24-Sep-2021.)

**Assertion**
Ref	Expression
ordtri3	⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴)))

**Proof of Theorem ordtri3**
Step	Hyp	Ref	Expression
1		ordirr 6335	. . . . . 6 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
2	1	adantl 481	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ¬ 𝐵 ∈ 𝐵)
3		eleq2 2825	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
4	3	notbid 318	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
5	2, 4	syl5ibrcom 247	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
6	5	pm4.71d 561	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)))
7		pm5.61 1002	. . . 4 ⊢ (((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∧ ¬ 𝐵 ∈ 𝐴) ↔ (𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))
8		pm4.52 986	. . . 4 ⊢ (((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∧ ¬ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴))
9	7, 8	bitr3i 277	. . 3 ⊢ ((𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴))
10	6, 9	bitrdi 287	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
11		ordtri2 6352	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
12	11	orbi1d 916	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
13	12	notbid 318	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
14	10, 13	bitr4d 282	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 Ord word 6316

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 2115 ax-9 2123 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

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 2715 df-cleq 2728 df-clel 2811 df-ne 2933 df-ral 3052 df-rex 3061 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-opab 5161 df-tr 5206 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-ord 6320

This theorem is referenced by: ordunisuc2 7786 tz7.48lem 8372 oacan 8475 omcan 8496 oecan 8517 omsmo 8586 omopthi 8589 inf3lem6 9542 cantnfp1lem3 9589 infpssrlem5 10217 fin23lem24 10232 isf32lem4 10266 om2uzf1oi 13876 om2noseqf1o 28297 ordnexbtwnsuc 43519

W3C validator