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

Theorem nnregexmid 4269
 Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4203 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 5990 or nntri3or 5987), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)
Hypothesis
Ref Expression
nnregexmid.1 ((x ⊆ 𝜔 y y x) → y(y x z(z y → ¬ z x)))
Assertion
Ref Expression
nnregexmid (φ ¬ φ)
Distinct variable group:   φ,x,y,z

Proof of Theorem nnregexmid
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 ssrab2 3002 . . . 4 {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ {∅, {∅}}
2 peano1 4244 . . . . 5 𝜔
3 suc0 4097 . . . . . 6 suc ∅ = {∅}
4 peano2 4245 . . . . . . 7 (∅ 𝜔 → suc ∅ 𝜔)
52, 4ax-mp 7 . . . . . 6 suc ∅ 𝜔
63, 5eqeltrri 2093 . . . . 5 {∅} 𝜔
7 prssi 3496 . . . . 5 ((∅ 𝜔 {∅} 𝜔) → {∅, {∅}} ⊆ 𝜔)
82, 6, 7mp2an 404 . . . 4 {∅, {∅}} ⊆ 𝜔
91, 8sstri 2931 . . 3 {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ 𝜔
10 eqid 2022 . . . 4 {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}
1110regexmidlemm 4201 . . 3 y y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}
12 pp0ex 3914 . . . . 5 {∅, {∅}} V
1312rabex 3875 . . . 4 {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} V
14 sseq1 2943 . . . . . 6 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (x ⊆ 𝜔 ↔ {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ 𝜔))
15 eleq2 2083 . . . . . . 7 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (y xy {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))
1615exbidv 1688 . . . . . 6 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (y y xy y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))
1714, 16anbi12d 445 . . . . 5 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → ((x ⊆ 𝜔 y y x) ↔ ({w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ 𝜔 y y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})))
18 eleq2 2083 . . . . . . . . . 10 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (z xz {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))
1918notbid 579 . . . . . . . . 9 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (¬ z x ↔ ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))
2019imbi2d 219 . . . . . . . 8 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → ((z y → ¬ z x) ↔ (z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})))
2120albidv 1687 . . . . . . 7 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (z(z y → ¬ z x) ↔ z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})))
2215, 21anbi12d 445 . . . . . 6 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → ((y x z(z y → ¬ z x)) ↔ (y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))))
2322exbidv 1688 . . . . 5 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (y(y x z(z y → ¬ z x)) ↔ y(y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))))
2417, 23imbi12d 223 . . . 4 (x = {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} → (((x ⊆ 𝜔 y y x) → y(y x z(z y → ¬ z x))) ↔ (({w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ 𝜔 y y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}) → y(y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})))))
25 nnregexmid.1 . . . 4 ((x ⊆ 𝜔 y y x) → y(y x z(z y → ¬ z x)))
2613, 24, 25vtocl 2585 . . 3 (({w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} ⊆ 𝜔 y y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}) → y(y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})))
279, 11, 26mp2an 404 . 2 y(y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))}))
2810regexmidlem1 4202 . 2 (y(y {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))} z(z y → ¬ z {w {∅, {∅}} ∣ (w = {∅} (w = ∅ φ))})) → (φ ¬ φ))
2927, 28ax-mp 7 1 (φ ¬ φ)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 616  ∀wal 1226   = wceq 1228  ∃wex 1362   ∈ wcel 1374  {crab 2288   ⊆ wss 2894  ∅c0 3201  {csn 3350  {cpr 3351  suc csuc 4051  𝜔com 4240 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-nul 3857  ax-pow 3901  ax-pr 3918  ax-un 4120 This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-rex 2290  df-rab 2293  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-uni 3555  df-int 3590  df-suc 4057  df-iom 4241 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator