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