Theorem elgch

Description: Elementhood in the collection of GCH-sets. (Contributed by Mario Carneiro, 15-May-2015)

	Ref	Expression
Assertion	elgch	|- ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-gch	|- GCH = ( Fin u. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } )
2	1	eleq2i	|- ( A e. GCH <-> A e. ( Fin u. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } ) )
3		elun	|- ( A e. ( Fin u. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } ) <-> ( A e. Fin \/ A e. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } ) )
4	2 3	bitri	|- ( A e. GCH <-> ( A e. Fin \/ A e. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } ) )
5		breq1	|- ( y = A -> ( y ~< x <-> A ~< x ) )
6		pweq	|- ( y = A -> ~P y = ~P A )
7	6	breq2d	|- ( y = A -> ( x ~< ~P y <-> x ~< ~P A ) )
8	5 7	anbi12d	|- ( y = A -> ( ( y ~< x /\ x ~< ~P y ) <-> ( A ~< x /\ x ~< ~P A ) ) )
9	8	notbid	|- ( y = A -> ( -. ( y ~< x /\ x ~< ~P y ) <-> -. ( A ~< x /\ x ~< ~P A ) ) )
10	9	albidv	|- ( y = A -> ( A. x -. ( y ~< x /\ x ~< ~P y ) <-> A. x -. ( A ~< x /\ x ~< ~P A ) ) )
11	10	elabg	|- ( A e. V -> ( A e. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } <-> A. x -. ( A ~< x /\ x ~< ~P A ) ) )
12	11	orbi2d	|- ( A e. V -> ( ( A e. Fin \/ A e. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } ) <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
13	4 12	syl5bb	|- ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )