Theorem gchi

Description: The only GCH-sets which have other sets between it and its power set are finite sets. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	gchi	|- ( ( A e. GCH /\ A ~< B /\ B ~< ~P A ) -> A e. Fin )

Proof

Step	Hyp	Ref	Expression
1		relsdom	|- Rel ~<
2	1	brrelex1i	|- ( B ~< ~P A -> B e. _V )
3	2	adantl	|- ( ( A ~< B /\ B ~< ~P A ) -> B e. _V )
4		breq2	|- ( x = B -> ( A ~< x <-> A ~< B ) )
5		breq1	|- ( x = B -> ( x ~< ~P A <-> B ~< ~P A ) )
6	4 5	anbi12d	|- ( x = B -> ( ( A ~< x /\ x ~< ~P A ) <-> ( A ~< B /\ B ~< ~P A ) ) )
7	6	spcegv	|- ( B e. _V -> ( ( A ~< B /\ B ~< ~P A ) -> E. x ( A ~< x /\ x ~< ~P A ) ) )
8	3 7	mpcom	|- ( ( A ~< B /\ B ~< ~P A ) -> E. x ( A ~< x /\ x ~< ~P A ) )
9		df-ex	|- ( E. x ( A ~< x /\ x ~< ~P A ) <-> -. A. x -. ( A ~< x /\ x ~< ~P A ) )
10	8 9	sylib	|- ( ( A ~< B /\ B ~< ~P A ) -> -. A. x -. ( A ~< x /\ x ~< ~P A ) )
11		elgch	|- ( A e. GCH -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
12	11	ibi	|- ( A e. GCH -> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) )
13	12	orcomd	|- ( A e. GCH -> ( A. x -. ( A ~< x /\ x ~< ~P A ) \/ A e. Fin ) )
14	13	ord	|- ( A e. GCH -> ( -. A. x -. ( A ~< x /\ x ~< ~P A ) -> A e. Fin ) )
15	10 14	syl5	|- ( A e. GCH -> ( ( A ~< B /\ B ~< ~P A ) -> A e. Fin ) )
16	15	3impib	|- ( ( A e. GCH /\ A ~< B /\ B ~< ~P A ) -> A e. Fin )