Theorem canth2g 7612

Description: Cantor's theorem with the sethood requirement expressed as an antecedent. Theorem 23 of [Suppes] p. 97. (Contributed by NM, 7-Nov-2003.)

Assertion

Ref	Expression
canth2g	|- ( A e. V -> A ~< ~P A )

Proof of Theorem canth2g

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pweq 3947	. . 3 |- ( x = A -> ~P x = ~P A )
2		breq12 4389	. . 3 |- ( ( x = A /\ ~P x = ~P A ) -> ( x ~< ~P x <-> A ~< ~P A ) )
3	1, 2	mpdan 666	. 2 |- ( x = A -> ( x ~< ~P x <-> A ~< ~P A ) )
4		vex 3054	. . 3 |- x e. _V
5	4	canth2 7611	. 2 |- x ~< ~P x
6	3, 5	vtoclg 3109	1 |- ( A e. V -> A ~< ~P A )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1399   e. wcel 1836   ~Pcpw 3944   class class class wbr 4384   ~< csdm 7456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-op 3968  df-uni 4181  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-en 7458  df-dom 7459  df-sdom 7460

This theorem is referenced by:  2pwuninel  7613  2pwne  7614  pwfi  7752  cdalepw  8511  isfin32i  8680  fin34  8705  hsmexlem1  8741  canth3  8871  ondomon  8873  gchdomtri  8940  canthp1lem1  8963  canthp1lem2  8964  pwfseqlem5  8974  gchcdaidm  8979  gchxpidm  8980  gchpwdom  8981  gchaclem  8989  gchhar  8990  tsksdom  9067