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 6382

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 6364	. . . . . 6 ⊢ (Ord 𝐵 → ¬ 𝐵 ∈ 𝐵)
2	1	adantl 485	. . . . 5 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ¬ 𝐵 ∈ 𝐵)
3		eleq2 2851	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐵 ∈ 𝐴 ↔ 𝐵 ∈ 𝐵))
4	3	notbid 320	. . . . 5 ⊢ (𝐴 = 𝐵 → (¬ 𝐵 ∈ 𝐴 ↔ ¬ 𝐵 ∈ 𝐵))
5	2, 4	syl5ibrcom 249	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 → ¬ 𝐵 ∈ 𝐴))
6	5	pm4.71d 569	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ (𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴)))
7		pm5.61 1014	. . . 4 ⊢ (((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∧ ¬ 𝐵 ∈ 𝐴) ↔ (𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))
8		pm4.52 998	. . . 4 ⊢ (((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∧ ¬ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴))
9	7, 8	bitr3i 279	. . 3 ⊢ ((𝐴 = 𝐵 ∧ ¬ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴))
10	6, 9	bitrdi 289	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
11		ordtri2 6381	. . . 4 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)))
12	11	orbi1d 927	. . 3 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
13	12	notbid 320	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ ¬ (¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ∨ 𝐵 ∈ 𝐴)))
14	10, 13	bitr4d 284	1 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ ¬ (𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 Ord word 6345

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 ax-sep 5246 ax-pr 5390

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-ne 2958 df-ral 3077 df-rex 3087 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-tr 5208 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-ord 6349

This theorem is referenced by: ordunisuc2 7824 tz7.48lem 8412 oacan 8517 omcan 8538 oecan 8559 omsmo 8628 omopthi 8631 inf3lem6 9588 cantnfp1lem3 9635 infpssrlem5 10264 fin23lem24 10279 isf32lem4 10313 om2uzf1oi 13966 om2noseqf1o 28394 mh-inf3f1 36901 ordnexbtwnsuc 43844

W3C validator