Metamath Proof Explorer

Theorem cardprclem

Description: Lemma for cardprc . (Contributed by Mario Carneiro, 22-Jan-2013) (Revised by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis cardprclem.1 
|- A = { x | ( card ` x ) = x }
Assertion cardprclem 
|- -. A e. _V

Proof

Step Hyp Ref Expression
1 cardprclem.1 
 |-  A = { x | ( card ` x ) = x }
2 1 eleq2i 
 |-  ( x e. A <-> x e. { x | ( card ` x ) = x } )
3 abid 
 |-  ( x e. { x | ( card ` x ) = x } <-> ( card ` x ) = x )
4 iscard 
 |-  ( ( card ` x ) = x <-> ( x e. On /\ A. y e. x y ~< x ) )
5 2 3 4 3bitri 
 |-  ( x e. A <-> ( x e. On /\ A. y e. x y ~< x ) )
6 5 simplbi 
 |-  ( x e. A -> x e. On )
7 6 ssriv 
 |-  A C_ On
8 ssonuni 
 |-  ( A e. _V -> ( A C_ On -> U. A e. On ) )
9 7 8 mpi 
 |-  ( A e. _V -> U. A e. On )
10 domrefg 
 |-  ( U. A e. On -> U. A ~<_ U. A )
11 9 10 syl 
 |-  ( A e. _V -> U. A ~<_ U. A )
12 elharval 
 |-  ( U. A e. ( har ` U. A ) <-> ( U. A e. On /\ U. A ~<_ U. A ) )
13 9 11 12 sylanbrc 
 |-  ( A e. _V -> U. A e. ( har ` U. A ) )
14 7 sseli 
 |-  ( z e. A -> z e. On )
15 domrefg 
 |-  ( z e. On -> z ~<_ z )
16 15 ancli 
 |-  ( z e. On -> ( z e. On /\ z ~<_ z ) )
17 elharval 
 |-  ( z e. ( har ` z ) <-> ( z e. On /\ z ~<_ z ) )
18 16 17 sylibr 
 |-  ( z e. On -> z e. ( har ` z ) )
19 14 18 syl 
 |-  ( z e. A -> z e. ( har ` z ) )
20 harcard 
 |-  ( card ` ( har ` z ) ) = ( har ` z )
21 fvex 
 |-  ( har ` z ) e. _V
22 fveq2 
 |-  ( x = ( har ` z ) -> ( card ` x ) = ( card ` ( har ` z ) ) )
23 id 
 |-  ( x = ( har ` z ) -> x = ( har ` z ) )
24 22 23 eqeq12d 
 |-  ( x = ( har ` z ) -> ( ( card ` x ) = x <-> ( card ` ( har ` z ) ) = ( har ` z ) ) )
25 21 24 1 elab2 
 |-  ( ( har ` z ) e. A <-> ( card ` ( har ` z ) ) = ( har ` z ) )
26 20 25 mpbir 
 |-  ( har ` z ) e. A
27 eleq2 
 |-  ( w = ( har ` z ) -> ( z e. w <-> z e. ( har ` z ) ) )
28 eleq1 
 |-  ( w = ( har ` z ) -> ( w e. A <-> ( har ` z ) e. A ) )
29 27 28 anbi12d 
 |-  ( w = ( har ` z ) -> ( ( z e. w /\ w e. A ) <-> ( z e. ( har ` z ) /\ ( har ` z ) e. A ) ) )
30 21 29 spcev 
 |-  ( ( z e. ( har ` z ) /\ ( har ` z ) e. A ) -> E. w ( z e. w /\ w e. A ) )
31 19 26 30 sylancl 
 |-  ( z e. A -> E. w ( z e. w /\ w e. A ) )
32 eluni 
 |-  ( z e. U. A <-> E. w ( z e. w /\ w e. A ) )
33 31 32 sylibr 
 |-  ( z e. A -> z e. U. A )
34 33 ssriv 
 |-  A C_ U. A
35 harcard 
 |-  ( card ` ( har ` U. A ) ) = ( har ` U. A )
36 fvex 
 |-  ( har ` U. A ) e. _V
37 fveq2 
 |-  ( x = ( har ` U. A ) -> ( card ` x ) = ( card ` ( har ` U. A ) ) )
38 id 
 |-  ( x = ( har ` U. A ) -> x = ( har ` U. A ) )
39 37 38 eqeq12d 
 |-  ( x = ( har ` U. A ) -> ( ( card ` x ) = x <-> ( card ` ( har ` U. A ) ) = ( har ` U. A ) ) )
40 36 39 1 elab2 
 |-  ( ( har ` U. A ) e. A <-> ( card ` ( har ` U. A ) ) = ( har ` U. A ) )
41 35 40 mpbir 
 |-  ( har ` U. A ) e. A
42 34 41 sselii 
 |-  ( har ` U. A ) e. U. A
43 13 42 jctir 
 |-  ( A e. _V -> ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
44 eloni 
 |-  ( U. A e. On -> Ord U. A )
45 ordn2lp 
 |-  ( Ord U. A -> -. ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
46 9 44 45 3syl 
 |-  ( A e. _V -> -. ( U. A e. ( har ` U. A ) /\ ( har ` U. A ) e. U. A ) )
47 43 46 pm2.65i 
 |-  -. A e. _V