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

Theorem ltcpw1pwg 6202
 Description: The cardinality of a unit power class is strictly less than the cardinality of the power class. Theorem XI.2.17 of [Rosser] p. 376. (Contributed by SF, 10-Mar-2015.)
Assertion
Ref Expression
ltcpw1pwg (A VNc 1A <c Nc A)

Proof of Theorem ltcpw1pwg
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pw1exg 4302 . . . . 5 (A V1A V)
2 ncidg 6122 . . . . 5 (1A V → 1A Nc 1A)
31, 2syl 15 . . . 4 (A V1A Nc 1A)
4 pwexg 4328 . . . . 5 (A VA V)
5 ncidg 6122 . . . . 5 (A V → A Nc A)
64, 5syl 15 . . . 4 (A VA Nc A)
7 pw1sspw 4171 . . . . 5 1A A
8 sseq1 3292 . . . . . 6 (x = 1A → (x y1A y))
9 sseq2 3293 . . . . . 6 (y = A → (1A y1A A))
108, 9rspc2ev 2963 . . . . 5 ((1A Nc 1A A Nc A 1A A) → x Nc 1Ay Nc Ax y)
117, 10mp3an3 1266 . . . 4 ((1A Nc 1A A Nc A) → x Nc 1Ay Nc Ax y)
123, 6, 11syl2anc 642 . . 3 (A Vx Nc 1Ay Nc Ax y)
13 ncex 6117 . . . 4 Nc 1A V
14 ncex 6117 . . . 4 Nc A V
1513, 14brlec 6113 . . 3 ( Nc 1Ac Nc Ax Nc 1Ay Nc Ax y)
1612, 15sylibr 203 . 2 (A VNc 1Ac Nc A)
17 ncpw1pwneg 6201 . 2 (A VNc 1ANc A)
18 brltc 6114 . 2 ( Nc 1A <c Nc A ↔ ( Nc 1Ac Nc A Nc 1ANc A))
1916, 17, 18sylanbrc 645 1 (A VNc 1A <c Nc A)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1710   ≠ wne 2516  ∃wrex 2615  Vcvv 2859   ⊆ wss 3257  ℘cpw 3722  ℘1cpw1 4135   class class class wbr 4639   ≤c clec 6089
 Copyright terms: Public domain W3C validator