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

Theorem nchoicelem5 6293
 Description: Lemma for nchoice 6308. A cardinal is not a member of the special set of itself raised to two. Theorem 6.5 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
Assertion
Ref Expression
nchoicelem5 ((M NC (Mc 0c) NC ) → ¬ M ( Spac ‘(2cc M)))

Proof of Theorem nchoicelem5
StepHypRef Expression
1 ce2lt 6220 . . . 4 ((M NC (Mc 0c) NC ) → M <c (2cc M))
2 2nc 6168 . . . . . . 7 2c NC
32jctl 525 . . . . . 6 (M NC → (2c NC M NC ))
4 2nnc 6167 . . . . . . . . 9 2c Nn
5 ce0nn 6180 . . . . . . . . 9 (2c Nn → (2cc 0c) ≠ )
64, 5ax-mp 5 . . . . . . . 8 (2cc 0c) ≠
7 ce0nulnc 6184 . . . . . . . . 9 (2c NC → ((2cc 0c) ≠ ↔ (2cc 0c) NC ))
82, 7ax-mp 5 . . . . . . . 8 ((2cc 0c) ≠ ↔ (2cc 0c) NC )
96, 8mpbi 199 . . . . . . 7 (2cc 0c) NC
109jctl 525 . . . . . 6 ((Mc 0c) NC → ((2cc 0c) NC (Mc 0c) NC ))
11 cecl 6186 . . . . . 6 (((2c NC M NC ) ((2cc 0c) NC (Mc 0c) NC )) → (2cc M) NC )
123, 10, 11syl2an 463 . . . . 5 ((M NC (Mc 0c) NC ) → (2cc M) NC )
13 ltlenlec 6207 . . . . 5 ((M NC (2cc M) NC ) → (M <c (2cc M) ↔ (Mc (2cc M) ¬ (2cc M) ≤c M)))
1412, 13syldan 456 . . . 4 ((M NC (Mc 0c) NC ) → (M <c (2cc M) ↔ (Mc (2cc M) ¬ (2cc M) ≤c M)))
151, 14mpbid 201 . . 3 ((M NC (Mc 0c) NC ) → (Mc (2cc M) ¬ (2cc M) ≤c M))
1615simprd 449 . 2 ((M NC (Mc 0c) NC ) → ¬ (2cc M) ≤c M)
17 nchoicelem4 6292 . . 3 (((2cc M) NC M ( Spac ‘(2cc M))) → (2cc M) ≤c M)
1812, 17sylan 457 . 2 (((M NC (Mc 0c) NC ) M ( Spac ‘(2cc M))) → (2cc M) ≤c M)
1916, 18mtand 640 1 ((M NC (Mc 0c) NC ) → ¬ M ( Spac ‘(2cc M)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358   ∈ wcel 1710   ≠ wne 2516  ∅c0 3550   Nn cnnc 4373  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