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

Theorem ce2lt 6220
 Description: Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of [Rosser] p. 390. (Contributed by SF, 13-Mar-2015.)
Assertion
Ref Expression
ce2lt ((M NC (Mc 0c) NC ) → M <c (2cc M))

Proof of Theorem ce2lt
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 ce0ncpw1 6185 . 2 ((M NC (Mc 0c) NC ) → x M = Nc 1x)
2 id 19 . . . . 5 (M = Nc 1xM = Nc 1x)
3 vex 2862 . . . . . 6 x V
4 ltcpw1pwg 6202 . . . . . 6 (x V → Nc 1x <c Nc x)
53, 4ax-mp 5 . . . . 5 Nc 1x <c Nc x
62, 5syl6eqbr 4676 . . . 4 (M = Nc 1xM <c Nc x)
73ce2 6192 . . . 4 (M = Nc 1x → (2cc M) = Nc x)
86, 7breqtrrd 4665 . . 3 (M = Nc 1xM <c (2cc M))
98exlimiv 1634 . 2 (x M = Nc 1xM <c (2cc M))
101, 9syl 15 1 ((M NC (Mc 0c) NC ) → M <c (2cc M))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 358  ∃wex 1541   = wceq 1642   ∈ wcel 1710  Vcvv 2859  ℘cpw 3722  ℘1cpw1 4135  0cc0c 4374   class class class wbr 4639  (class class class)co 5525   NC cncs 6088
 Copyright terms: Public domain W3C validator