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

Theorem elni2 6174
Description: Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
Assertion
Ref Expression
elni2 (A N ↔ (A 𝜔 A))

Proof of Theorem elni2
StepHypRef Expression
1 pinn 6169 . . 3 (A NA 𝜔)
2 0npi 6173 . . . . . 6 ¬ ∅ N
3 eleq1 2082 . . . . . 6 (A = ∅ → (A N ↔ ∅ N))
42, 3mtbiri 587 . . . . 5 (A = ∅ → ¬ A N)
54con2i 545 . . . 4 (A N → ¬ A = ∅)
6 0elnn 4267 . . . . . 6 (A 𝜔 → (A = ∅ A))
71, 6syl 14 . . . . 5 (A N → (A = ∅ A))
87ord 630 . . . 4 (A N → (¬ A = ∅ → ∅ A))
95, 8mpd 13 . . 3 (A N → ∅ A)
101, 9jca 290 . 2 (A N → (A 𝜔 A))
11 nndceq0 4266 . . . . . 6 (A 𝜔 → DECID A = ∅)
12 df-dc 734 . . . . . 6 (DECID A = ∅ ↔ (A = ∅ ¬ A = ∅))
1311, 12sylib 127 . . . . 5 (A 𝜔 → (A = ∅ ¬ A = ∅))
1413anim1i 323 . . . 4 ((A 𝜔 A) → ((A = ∅ ¬ A = ∅) A))
15 ancom 253 . . . . 5 ((∅ A (A = ∅ ¬ A = ∅)) ↔ ((A = ∅ ¬ A = ∅) A))
16 andi 719 . . . . 5 ((∅ A (A = ∅ ¬ A = ∅)) ↔ ((∅ A A = ∅) (∅ A ¬ A = ∅)))
1715, 16bitr3i 175 . . . 4 (((A = ∅ ¬ A = ∅) A) ↔ ((∅ A A = ∅) (∅ A ¬ A = ∅)))
1814, 17sylib 127 . . 3 ((A 𝜔 A) → ((∅ A A = ∅) (∅ A ¬ A = ∅)))
19 noel 3205 . . . . . . . . 9 ¬ ∅
20 eleq2 2083 . . . . . . . . 9 (A = ∅ → (∅ A ↔ ∅ ∅))
2119, 20mtbiri 587 . . . . . . . 8 (A = ∅ → ¬ ∅ A)
2221pm2.21d 537 . . . . . . 7 (A = ∅ → (∅ AA N))
2322impcom 116 . . . . . 6 ((∅ A A = ∅) → A N)
2423a1i 9 . . . . 5 (A 𝜔 → ((∅ A A = ∅) → A N))
25 df-ne 2188 . . . . . . 7 (A ≠ ∅ ↔ ¬ A = ∅)
26 elni 6168 . . . . . . . 8 (A N ↔ (A 𝜔 A ≠ ∅))
2726simplbi2 367 . . . . . . 7 (A 𝜔 → (A ≠ ∅ → A N))
2825, 27syl5bir 142 . . . . . 6 (A 𝜔 → (¬ A = ∅ → A N))
2928adantld 263 . . . . 5 (A 𝜔 → ((∅ A ¬ A = ∅) → A N))
3024, 29jaod 624 . . . 4 (A 𝜔 → (((∅ A A = ∅) (∅ A ¬ A = ∅)) → A N))
3130adantr 261 . . 3 ((A 𝜔 A) → (((∅ A A = ∅) (∅ A ¬ A = ∅)) → A N))
3218, 31mpd 13 . 2 ((A 𝜔 A) → A N)
3310, 32impbii 117 1 (A N ↔ (A 𝜔 A))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97  wb 98   wo 616  DECID wdc 733   = wceq 1228   wcel 1374  wne 2186  c0 3201  𝜔com 4240  Ncnpi 6130
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  ax-iinf 4238
This theorem depends on definitions:  df-bi 110  df-dc 734  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-ne 2188  df-ral 2289  df-rex 2290  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  df-ni 6164
This theorem is referenced by:  addclpi  6187  mulclpi  6188  mulcanpig  6195  addnidpig  6196  ltexpi  6197  ltmpig  6199  nnppipi  6202  archnqq  6274  enq0tr  6289
  Copyright terms: Public domain W3C validator