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

Metamath Proof Explorer

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 bitrid 
 |-  ( A e. V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )