This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hargch

Description: If A + ~~P A , then A is a GCH-set. The much simpler converse to gchhar . (Contributed by Mario Carneiro, 2-Jun-2015)

Ref Expression
Assertion hargch 
|- ( ( har ` A ) ~~ ~P A -> A e. GCH )

Proof

Step Hyp Ref Expression
1 harcl 
 |-  ( har ` A ) e. On
2 sdomdom 
 |-  ( x ~< ( har ` A ) -> x ~<_ ( har ` A ) )
3 ondomen 
 |-  ( ( ( har ` A ) e. On /\ x ~<_ ( har ` A ) ) -> x e. dom card )
4 1 2 3 sylancr 
 |-  ( x ~< ( har ` A ) -> x e. dom card )
5 onenon 
 |-  ( ( har ` A ) e. On -> ( har ` A ) e. dom card )
6 1 5 ax-mp 
 |-  ( har ` A ) e. dom card
7 cardsdom2 
 |-  ( ( x e. dom card /\ ( har ` A ) e. dom card ) -> ( ( card ` x ) e. ( card ` ( har ` A ) ) <-> x ~< ( har ` A ) ) )
8 4 6 7 sylancl 
 |-  ( x ~< ( har ` A ) -> ( ( card ` x ) e. ( card ` ( har ` A ) ) <-> x ~< ( har ` A ) ) )
9 8 ibir 
 |-  ( x ~< ( har ` A ) -> ( card ` x ) e. ( card ` ( har ` A ) ) )
10 harcard 
 |-  ( card ` ( har ` A ) ) = ( har ` A )
11 9 10 eleqtrdi 
 |-  ( x ~< ( har ` A ) -> ( card ` x ) e. ( har ` A ) )
12 elharval 
 |-  ( ( card ` x ) e. ( har ` A ) <-> ( ( card ` x ) e. On /\ ( card ` x ) ~<_ A ) )
13 12 simprbi 
 |-  ( ( card ` x ) e. ( har ` A ) -> ( card ` x ) ~<_ A )
14 11 13 syl 
 |-  ( x ~< ( har ` A ) -> ( card ` x ) ~<_ A )
15 cardid2 
 |-  ( x e. dom card -> ( card ` x ) ~~ x )
16 domen1 
 |-  ( ( card ` x ) ~~ x -> ( ( card ` x ) ~<_ A <-> x ~<_ A ) )
17 4 15 16 3syl 
 |-  ( x ~< ( har ` A ) -> ( ( card ` x ) ~<_ A <-> x ~<_ A ) )
18 14 17 mpbid 
 |-  ( x ~< ( har ` A ) -> x ~<_ A )
19 domnsym 
 |-  ( x ~<_ A -> -. A ~< x )
20 18 19 syl 
 |-  ( x ~< ( har ` A ) -> -. A ~< x )
21 20 con2i 
 |-  ( A ~< x -> -. x ~< ( har ` A ) )
22 sdomen2 
 |-  ( ( har ` A ) ~~ ~P A -> ( x ~< ( har ` A ) <-> x ~< ~P A ) )
23 22 notbid 
 |-  ( ( har ` A ) ~~ ~P A -> ( -. x ~< ( har ` A ) <-> -. x ~< ~P A ) )
24 21 23 imbitrid 
 |-  ( ( har ` A ) ~~ ~P A -> ( A ~< x -> -. x ~< ~P A ) )
25 imnan 
 |-  ( ( A ~< x -> -. x ~< ~P A ) <-> -. ( A ~< x /\ x ~< ~P A ) )
26 24 25 sylib 
 |-  ( ( har ` A ) ~~ ~P A -> -. ( A ~< x /\ x ~< ~P A ) )
27 26 alrimiv 
 |-  ( ( har ` A ) ~~ ~P A -> A. x -. ( A ~< x /\ x ~< ~P A ) )
28 27 olcd 
 |-  ( ( har ` A ) ~~ ~P A -> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) )
29 relen 
 |-  Rel ~~
30 29 brrelex2i 
 |-  ( ( har ` A ) ~~ ~P A -> ~P A e. _V )
31 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
32 30 31 sylibr 
 |-  ( ( har ` A ) ~~ ~P A -> A e. _V )
33 elgch 
 |-  ( A e. _V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
34 32 33 syl 
 |-  ( ( har ` A ) ~~ ~P A -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
35 28 34 mpbird 
 |-  ( ( har ` A ) ~~ ~P A -> A e. GCH )