Theorem onntri35 7348

Description: Double negated ordinal trichotomy.

There are five equivalent statements: (1) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (2) ¬ ¬ ∀𝑥 ∈ On∀𝑦 ∈ On(𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), (3) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥), (4) ∀𝑥 ∈ On∀𝑦 ∈ On¬ ¬ (𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥), and (5) ¬ ¬ EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7349), (3) implies (5) (onntri35 7348), (5) implies (1) (onntri51 7351), (2) implies (4) (onntri24 7353), (4) implies (5) (onntri45 7352), and (5) implies (2) (onntri52 7355).

Another way of stating this is that EXMID is equivalent to trichotomy, either the 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 or the 𝑥 ⊆ 𝑦 ∨ 𝑦 ⊆ 𝑥 form, as shown in exmidontri 7350 and exmidontri2or 7354, respectively. Thus ¬ ¬ EXMID is equivalent to (1) or (2). In addition, ¬ ¬ EXMID is equivalent to (3) by onntri3or 7356 and (4) by onntri2or 7357.

(Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

Assertion

Ref	Expression
onntri35	⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ EXMID)

Distinct variable group:   𝑥,𝑦

Proof of Theorem onntri35

Step	Hyp	Ref	Expression
1		pw1on 7337	. . . . 5 ⊢ 𝒫 1o ∈ On
2	1	onsuci 4563	. . . 4 ⊢ suc 𝒫 1o ∈ On
3		3on 6512	. . . 4 ⊢ 3o ∈ On
4		eleq1 2267	. . . . . . . 8 ⊢ (𝑥 = suc 𝒫 1o → (𝑥 ∈ 𝑦 ↔ suc 𝒫 1o ∈ 𝑦))
5		eqeq1 2211	. . . . . . . 8 ⊢ (𝑥 = suc 𝒫 1o → (𝑥 = 𝑦 ↔ suc 𝒫 1o = 𝑦))
6		eleq2 2268	. . . . . . . 8 ⊢ (𝑥 = suc 𝒫 1o → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ suc 𝒫 1o))
7	4, 5, 6	3orbi123d 1323	. . . . . . 7 ⊢ (𝑥 = suc 𝒫 1o → ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o)))
8	7	notbid 668	. . . . . 6 ⊢ (𝑥 = suc 𝒫 1o → (¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ¬ (suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o)))
9	8	notbid 668	. . . . 5 ⊢ (𝑥 = suc 𝒫 1o → (¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ¬ ¬ (suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o)))
10		eleq2 2268	. . . . . . . 8 ⊢ (𝑦 = 3o → (suc 𝒫 1o ∈ 𝑦 ↔ suc 𝒫 1o ∈ 3o))
11		eqeq2 2214	. . . . . . . 8 ⊢ (𝑦 = 3o → (suc 𝒫 1o = 𝑦 ↔ suc 𝒫 1o = 3o))
12		eleq1 2267	. . . . . . . 8 ⊢ (𝑦 = 3o → (𝑦 ∈ suc 𝒫 1o ↔ 3o ∈ suc 𝒫 1o))
13	10, 11, 12	3orbi123d 1323	. . . . . . 7 ⊢ (𝑦 = 3o → ((suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o) ↔ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o)))
14	13	notbid 668	. . . . . 6 ⊢ (𝑦 = 3o → (¬ (suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o) ↔ ¬ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o)))
15	14	notbid 668	. . . . 5 ⊢ (𝑦 = 3o → (¬ ¬ (suc 𝒫 1o ∈ 𝑦 ∨ suc 𝒫 1o = 𝑦 ∨ 𝑦 ∈ suc 𝒫 1o) ↔ ¬ ¬ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o)))
16	9, 15	rspc2v 2889	. . . 4 ⊢ ((suc 𝒫 1o ∈ On ∧ 3o ∈ On) → (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o)))
17	2, 3, 16	mp2an 426	. . 3 ⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o))
18		3ioran 995	. . 3 ⊢ (¬ (suc 𝒫 1o ∈ 3o ∨ suc 𝒫 1o = 3o ∨ 3o ∈ suc 𝒫 1o) ↔ (¬ suc 𝒫 1o ∈ 3o ∧ ¬ suc 𝒫 1o = 3o ∧ ¬ 3o ∈ suc 𝒫 1o))
19	17, 18	sylnib 677	. 2 ⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ (¬ suc 𝒫 1o ∈ 3o ∧ ¬ suc 𝒫 1o = 3o ∧ ¬ 3o ∈ suc 𝒫 1o))
20		sucpw1nel3 7344	. . . 4 ⊢ ¬ suc 𝒫 1o ∈ 3o
21	20	a1i 9	. . 3 ⊢ (¬ EXMID → ¬ suc 𝒫 1o ∈ 3o)
22		2on 6510	. . . . . . 7 ⊢ 2o ∈ On
23		suc11 4605	. . . . . . 7 ⊢ ((𝒫 1o ∈ On ∧ 2o ∈ On) → (suc 𝒫 1o = suc 2o ↔ 𝒫 1o = 2o))
24	1, 22, 23	mp2an 426	. . . . . 6 ⊢ (suc 𝒫 1o = suc 2o ↔ 𝒫 1o = 2o)
25		df-3o 6503	. . . . . . 7 ⊢ 3o = suc 2o
26	25	eqeq2i 2215	. . . . . 6 ⊢ (suc 𝒫 1o = 3o ↔ suc 𝒫 1o = suc 2o)
27		exmidpweq 7005	. . . . . 6 ⊢ (EXMID ↔ 𝒫 1o = 2o)
28	24, 26, 27	3bitr4ri 213	. . . . 5 ⊢ (EXMID ↔ suc 𝒫 1o = 3o)
29	28	notbii 669	. . . 4 ⊢ (¬ EXMID ↔ ¬ suc 𝒫 1o = 3o)
30	29	biimpi 120	. . 3 ⊢ (¬ EXMID → ¬ suc 𝒫 1o = 3o)
31		3nelsucpw1 7345	. . . 4 ⊢ ¬ 3o ∈ suc 𝒫 1o
32	31	a1i 9	. . 3 ⊢ (¬ EXMID → ¬ 3o ∈ suc 𝒫 1o)
33	21, 30, 32	3jca 1179	. 2 ⊢ (¬ EXMID → (¬ suc 𝒫 1o ∈ 3o ∧ ¬ suc 𝒫 1o = 3o ∧ ¬ 3o ∈ suc 𝒫 1o))
34	19, 33	nsyl 629	1 ⊢ (∀𝑥 ∈ On ∀𝑦 ∈ On ¬ ¬ (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ¬ ¬ EXMID)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ w3o 979   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  ∀wral 2483  𝒫 cpw 3615  EXMIDwem 4237  Oncon0 4409  suc csuc 4411  1_oc1o 6494  2_oc2o 6495  3_oc3o 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-nul 4169  ax-pow 4217  ax-pr 4252  ax-un 4479  ax-setind 4584

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rex 2489  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-pr 3639  df-uni 3850  df-int 3885  df-tr 4142  df-exmid 4238  df-iord 4412  df-on 4414  df-suc 4417  df-iom 4638  df-1o 6501  df-2o 6502  df-3o 6503

This theorem is referenced by:  onntri3or  7356