ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ontri2orexmidim GIF version

Theorem ontri2orexmidim 4565
Description: Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4564. (Contributed by Jim Kingdon, 26-Aug-2024.)
Assertion
Ref Expression
ontri2orexmidim (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → DECID 𝜑)
Distinct variable group:   𝜑,𝑥,𝑦

Proof of Theorem ontri2orexmidim
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ordtri2or2exmidlem 4519 . . . . 5 {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ∈ On
2 suc0 4405 . . . . . 6 suc ∅ = {∅}
3 0elon 4386 . . . . . . 7 ∅ ∈ On
43onsuci 4509 . . . . . 6 suc ∅ ∈ On
52, 4eqeltrri 2249 . . . . 5 {∅} ∈ On
6 sseq1 3176 . . . . . . 7 (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑥𝑦 ↔ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦))
7 sseq2 3177 . . . . . . 7 (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → (𝑦𝑥𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))
86, 7orbi12d 793 . . . . . 6 (𝑥 = {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → ((𝑥𝑦𝑦𝑥) ↔ ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})))
9 sseq2 3177 . . . . . . 7 (𝑦 = {∅} → ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦 ↔ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅}))
10 sseq1 3176 . . . . . . 7 (𝑦 = {∅} → (𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))
119, 10orbi12d 793 . . . . . 6 (𝑦 = {∅} → (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ 𝑦𝑦 ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}) ↔ ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})))
128, 11rspc2va 2853 . . . . 5 ((({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ∈ On ∧ {∅} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥)) → ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))
131, 5, 12mpanl12 436 . . . 4 (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))
145onirri 4536 . . . . . 6 ¬ {∅} ∈ {∅}
15 simpl 109 . . . . . . . 8 (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∧ 𝜑) → {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅})
16 simpr 110 . . . . . . . . 9 (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∧ 𝜑) → 𝜑)
17 p0ex 4183 . . . . . . . . . . 11 {∅} ∈ V
1817prid2 3696 . . . . . . . . . 10 {∅} ∈ {∅, {∅}}
19 biidd 172 . . . . . . . . . . 11 (𝑧 = {∅} → (𝜑𝜑))
2019elrab3 2892 . . . . . . . . . 10 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑))
2118, 20ax-mp 5 . . . . . . . . 9 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑)
2216, 21sylibr 134 . . . . . . . 8 (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∧ 𝜑) → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})
2315, 22sseldd 3154 . . . . . . 7 (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∧ 𝜑) → {∅} ∈ {∅})
2423ex 115 . . . . . 6 ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} → (𝜑 → {∅} ∈ {∅}))
2514, 24mtoi 664 . . . . 5 ({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} → ¬ 𝜑)
26 snssg 3723 . . . . . . 7 (∅ ∈ On → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}))
273, 26ax-mp 5 . . . . . 6 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑})
28 0ex 4125 . . . . . . . 8 ∅ ∈ V
2928prid1 3695 . . . . . . 7 ∅ ∈ {∅, {∅}}
30 biidd 172 . . . . . . . 8 (𝑧 = ∅ → (𝜑𝜑))
3130elrab3 2892 . . . . . . 7 (∅ ∈ {∅, {∅}} → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑))
3229, 31ax-mp 5 . . . . . 6 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} ↔ 𝜑)
3327, 32sylbb1 137 . . . . 5 ({∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑} → 𝜑)
3425, 33orim12i 759 . . . 4 (({𝑧 ∈ {∅, {∅}} ∣ 𝜑} ⊆ {∅} ∨ {∅} ⊆ {𝑧 ∈ {∅, {∅}} ∣ 𝜑}) → (¬ 𝜑𝜑))
3513, 34syl 14 . . 3 (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → (¬ 𝜑𝜑))
3635orcomd 729 . 2 (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → (𝜑 ∨ ¬ 𝜑))
37 df-dc 835 . 2 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
3836, 37sylibr 134 1 (∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦𝑦𝑥) → DECID 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  wo 708  DECID wdc 834   = wceq 1353  wcel 2146  wral 2453  {crab 2457  wss 3127  c0 3420  {csn 3589  {cpr 3590  Oncon0 4357  suc csuc 4359
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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-setind 4530
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ne 2346  df-ral 2458  df-rex 2459  df-rab 2462  df-v 2737  df-dif 3129  df-un 3131  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595  df-pr 3596  df-uni 3806  df-tr 4097  df-iord 4360  df-on 4362  df-suc 4365
This theorem is referenced by:  exmidontri2or  7232
  Copyright terms: Public domain W3C validator