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

Theorem nchoicelem4 6292
 Description: Lemma for nchoice 6308. The initial value of Spac is a minimum value. Theorem 6.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
Assertion
Ref Expression
nchoicelem4 ((M NC N ( SpacM)) → Mc N)

Proof of Theorem nchoicelem4
Dummy variables n p are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasn 5018 . . 3 ( ≤c “ {M}) = {p Mc p}
2 lecex 6115 . . . 4 c V
3 snex 4111 . . . 4 {M} V
42, 3imaex 4747 . . 3 ( ≤c “ {M}) V
51, 4eqeltrri 2424 . 2 {p Mc p} V
6 breq2 4643 . 2 (p = M → (Mc pMc M))
7 breq2 4643 . 2 (p = n → (Mc pMc n))
8 breq2 4643 . 2 (p = (2cc n) → (Mc pMc (2cc n)))
9 breq2 4643 . 2 (p = N → (Mc pMc N))
10 nclecid 6197 . 2 (M NCMc M)
11 spacssnc 6284 . . . . . . 7 (M NC → ( SpacM) NC )
1211sselda 3273 . . . . . 6 ((M NC n ( SpacM)) → n NC )
13 ce2lt 6220 . . . . . 6 ((n NC (nc 0c) NC ) → n <c (2cc n))
1412, 13sylan 457 . . . . 5 (((M NC n ( SpacM)) (nc 0c) NC ) → n <c (2cc n))
15 brltc 6114 . . . . . 6 (n <c (2cc n) ↔ (nc (2cc n) n ≠ (2cc n)))
1615simplbi 446 . . . . 5 (n <c (2cc n) → nc (2cc n))
1714, 16syl 15 . . . 4 (((M NC n ( SpacM)) (nc 0c) NC ) → nc (2cc n))
18 simpll 730 . . . . 5 (((M NC n ( SpacM)) (nc 0c) NC ) → M NC )
1912adantr 451 . . . . 5 (((M NC n ( SpacM)) (nc 0c) NC ) → n NC )
20 2nnc 6167 . . . . . . 7 2c Nn
21 ceclnn1 6189 . . . . . . 7 ((2c Nn n NC (nc 0c) NC ) → (2cc n) NC )
2220, 21mp3an1 1264 . . . . . 6 ((n NC (nc 0c) NC ) → (2cc n) NC )
2312, 22sylan 457 . . . . 5 (((M NC n ( SpacM)) (nc 0c) NC ) → (2cc n) NC )
24 lectr 6211 . . . . 5 ((M NC n NC (2cc n) NC ) → ((Mc n nc (2cc n)) → Mc (2cc n)))
2518, 19, 23, 24syl3anc 1182 . . . 4 (((M NC n ( SpacM)) (nc 0c) NC ) → ((Mc n nc (2cc n)) → Mc (2cc n)))
2617, 25mpan2d 655 . . 3 (((M NC n ( SpacM)) (nc 0c) NC ) → (Mc nMc (2cc n)))
2726impr 602 . 2 (((M NC n ( SpacM)) ((nc 0c) NC Mc n)) → Mc (2cc n))
285, 6, 7, 8, 9, 10, 27spacis 6288 1 ((M NC N ( SpacM)) → Mc N)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358   ∈ wcel 1710  {cab 2339   ≠ wne 2516  Vcvv 2859  {csn 3737   Nn cnnc 4373  0cc0c 4374   class class class wbr 4639   “ cima 4722   ‘cfv 4781  (class class class)co 5525   NC cncs 6088   ≤c clec 6089
 Copyright terms: Public domain W3C validator