Metamath Proof Explorer

Theorem engch

Description: The property of being a GCH-set is a cardinal invariant. (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Assertion engch 
|- ( A ~~ B -> ( A e. GCH <-> B e. GCH ) )

Proof

Step Hyp Ref Expression
1 enfi 
 |-  ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )
2 sdomen1 
 |-  ( A ~~ B -> ( A ~< x <-> B ~< x ) )
3 pwen 
 |-  ( A ~~ B -> ~P A ~~ ~P B )
4 sdomen2 
 |-  ( ~P A ~~ ~P B -> ( x ~< ~P A <-> x ~< ~P B ) )
5 3 4 syl 
 |-  ( A ~~ B -> ( x ~< ~P A <-> x ~< ~P B ) )
6 2 5 anbi12d 
 |-  ( A ~~ B -> ( ( A ~< x /\ x ~< ~P A ) <-> ( B ~< x /\ x ~< ~P B ) ) )
7 6 notbid 
 |-  ( A ~~ B -> ( -. ( A ~< x /\ x ~< ~P A ) <-> -. ( B ~< x /\ x ~< ~P B ) ) )
8 7 albidv 
 |-  ( A ~~ B -> ( A. x -. ( A ~< x /\ x ~< ~P A ) <-> A. x -. ( B ~< x /\ x ~< ~P B ) ) )
9 1 8 orbi12d 
 |-  ( A ~~ B -> ( ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) <-> ( B e. Fin \/ A. x -. ( B ~< x /\ x ~< ~P B ) ) ) )
10 relen 
 |-  Rel ~~
11 10 brrelex1i 
 |-  ( A ~~ B -> A e. _V )
12 elgch 
 |-  ( A e. _V -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
13 11 12 syl 
 |-  ( A ~~ B -> ( A e. GCH <-> ( A e. Fin \/ A. x -. ( A ~< x /\ x ~< ~P A ) ) ) )
14 10 brrelex2i 
 |-  ( A ~~ B -> B e. _V )
15 elgch 
 |-  ( B e. _V -> ( B e. GCH <-> ( B e. Fin \/ A. x -. ( B ~< x /\ x ~< ~P B ) ) ) )
16 14 15 syl 
 |-  ( A ~~ B -> ( B e. GCH <-> ( B e. Fin \/ A. x -. ( B ~< x /\ x ~< ~P B ) ) ) )
17 9 13 16 3bitr4d 
 |-  ( A ~~ B -> ( A e. GCH <-> B e. GCH ) )