New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nmembers1lem2 GIF version

Theorem nmembers1lem2 6269
 Description: Lemma for nmembers1 6271. The set of all elements between one and zero is empty. (Contributed by Scott Fenton, 1-Aug-2019.)
Assertion
Ref Expression
nmembers1lem2 {m Nn (1cc m mc 0c)} 0c

Proof of Theorem nmembers1lem2
StepHypRef Expression
1 0lt1c 6258 . . . . . . . 8 0c <c 1c
2 0cnc 6138 . . . . . . . . 9 0c NC
3 1cnc 6139 . . . . . . . . 9 1c NC
4 ltlenlec 6207 . . . . . . . . 9 ((0c NC 1c NC ) → (0c <c 1c ↔ (0cc 1c ¬ 1cc 0c)))
52, 3, 4mp2an 653 . . . . . . . 8 (0c <c 1c ↔ (0cc 1c ¬ 1cc 0c))
61, 5mpbi 199 . . . . . . 7 (0cc 1c ¬ 1cc 0c)
76simpri 448 . . . . . 6 ¬ 1cc 0c
8 nnnc 6146 . . . . . . . . 9 (m Nnm NC )
9 lectr 6211 . . . . . . . . . 10 ((1c NC m NC 0c NC ) → ((1cc m mc 0c) → 1cc 0c))
103, 2, 9mp3an13 1268 . . . . . . . . 9 (m NC → ((1cc m mc 0c) → 1cc 0c))
118, 10syl 15 . . . . . . . 8 (m Nn → ((1cc m mc 0c) → 1cc 0c))
1211exp3a 425 . . . . . . 7 (m Nn → (1cc m → (mc 0c → 1cc 0c)))
1312imp 418 . . . . . 6 ((m Nn 1cc m) → (mc 0c → 1cc 0c))
147, 13mtoi 169 . . . . 5 ((m Nn 1cc m) → ¬ mc 0c)
1514ex 423 . . . 4 (m Nn → (1cc m → ¬ mc 0c))
16 imnan 411 . . . 4 ((1cc m → ¬ mc 0c) ↔ ¬ (1cc m mc 0c))
1715, 16sylib 188 . . 3 (m Nn → ¬ (1cc m mc 0c))
1817rgen 2679 . 2 m Nn ¬ (1cc m mc 0c)
19 el0c 4421 . . 3 ({m Nn (1cc m mc 0c)} 0c ↔ {m Nn (1cc m mc 0c)} = )
20 rabeq0 3572 . . 3 ({m Nn (1cc m mc 0c)} = m Nn ¬ (1cc m mc 0c))
2119, 20bitri 240 . 2 ({m Nn (1cc m mc 0c)} 0cm Nn ¬ (1cc m mc 0c))
2218, 21mpbir 200 1 {m Nn (1cc m mc 0c)} 0c
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ∈ wcel 1710  ∀wral 2614  {crab 2618  ∅c0 3550  1cc1c 4134   Nn cnnc 4373  0cc0c 4374   class class class wbr 4639   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator