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	syl5ib	|- ( ( 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 )