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 = z -> ( y ~< x <-> z ~< x ) )
6		pweq	|- ( y = z -> ~P y = ~P z )
7	6	breq2d	|- ( y = z -> ( x ~< ~P y <-> x ~< ~P z ) )
8	5 7	anbi12d	|- ( y = z -> ( ( y ~< x /\ x ~< ~P y ) <-> ( z ~< x /\ x ~< ~P z ) ) )
9	8	notbid	|- ( y = z -> ( -. ( y ~< x /\ x ~< ~P y ) <-> -. ( z ~< x /\ x ~< ~P z ) ) )
10	9	albidv	|- ( y = z -> ( A. x -. ( y ~< x /\ x ~< ~P y ) <-> A. x -. ( z ~< x /\ x ~< ~P z ) ) )
11		breq1	|- ( z = A -> ( z ~< x <-> A ~< x ) )
12		pweq	|- ( z = A -> ~P z = ~P A )
13	12	breq2d	|- ( z = A -> ( x ~< ~P z <-> x ~< ~P A ) )
14	11 13	anbi12d	|- ( z = A -> ( ( z ~< x /\ x ~< ~P z ) <-> ( A ~< x /\ x ~< ~P A ) ) )
15	14	notbid	|- ( z = A -> ( -. ( z ~< x /\ x ~< ~P z ) <-> -. ( A ~< x /\ x ~< ~P A ) ) )
16	15	albidv	|- ( z = A -> ( A. x -. ( z ~< x /\ x ~< ~P z ) <-> A. x -. ( A ~< x /\ x ~< ~P A ) ) )
17	10 16	elabgw	|- ( A e. V -> ( A e. { y | A. x -. ( y ~< x /\ x ~< ~P y ) } <-> A. x -. ( A ~< x /\ x ~< ~P A ) ) )
18	17	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 ) ) ) )
19	4 18	syl5bb	|- ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )