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

Theorem nchoicelem15 6303
 Description: Lemma for nchoice 6308. When the special set generator does not yield a singleton, then the cardinal is raisable. (Contributed by SF, 19-Mar-2015.)
Assertion
Ref Expression
nchoicelem15 ((M NC 1c <c Nc ( SpacM)) → (Mc 0c) NC )

Proof of Theorem nchoicelem15
StepHypRef Expression
1 brltc 6114 . . . 4 (1c <c Nc ( SpacM) ↔ (1cc Nc ( SpacM) 1cNc ( SpacM)))
21simprbi 450 . . 3 (1c <c Nc ( SpacM) → 1cNc ( SpacM))
3 df1c3g 6141 . . . . . . 7 (M NC → 1c = Nc {M})
43adantr 451 . . . . . 6 ((M NC ¬ (Mc 0c) NC ) → 1c = Nc {M})
5 nchoicelem3 6291 . . . . . . 7 ((M NC ¬ (Mc 0c) NC ) → ( SpacM) = {M})
65nceqd 6110 . . . . . 6 ((M NC ¬ (Mc 0c) NC ) → Nc ( SpacM) = Nc {M})
74, 6eqtr4d 2388 . . . . 5 ((M NC ¬ (Mc 0c) NC ) → 1c = Nc ( SpacM))
87ex 423 . . . 4 (M NC → (¬ (Mc 0c) NC → 1c = Nc ( SpacM)))
98necon1ad 2583 . . 3 (M NC → (1cNc ( SpacM) → (Mc 0c) NC ))
102, 9syl5 28 . 2 (M NC → (1c <c Nc ( SpacM) → (Mc 0c) NC ))
1110imp 418 1 ((M NC 1c <c Nc ( SpacM)) → (Mc 0c) NC )
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 358   = wceq 1642   ∈ wcel 1710   ≠ wne 2516  {csn 3737  1cc1c 4134  0cc0c 4374   class class class wbr 4639   ‘cfv 4781  (class class class)co 5525   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator