Metamath Proof Explorer

Theorem gchina

Description: Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of TakeutiZaring p. 106. (Contributed by Mario Carneiro, 5-Jun-2015)

Ref Expression
Assertion gchina 
|- ( GCH = _V -> InaccW = Inacc )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> x e. InaccW )
2 idd 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> ( x =/= (/) -> x =/= (/) ) )
3 idd 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> ( ( cf ` x ) = x -> ( cf ` x ) = x ) )
4 pwfi 
 |-  ( y e. Fin <-> ~P y e. Fin )
5 isfinite 
 |-  ( ~P y e. Fin <-> ~P y ~< _om )
6 winainf 
 |-  ( x e. InaccW -> _om C_ x )
7 ssdomg 
 |-  ( x e. InaccW -> ( _om C_ x -> _om ~<_ x ) )
8 6 7 mpd 
 |-  ( x e. InaccW -> _om ~<_ x )
9 sdomdomtr 
 |-  ( ( ~P y ~< _om /\ _om ~<_ x ) -> ~P y ~< x )
10 9 expcom 
 |-  ( _om ~<_ x -> ( ~P y ~< _om -> ~P y ~< x ) )
11 8 10 syl 
 |-  ( x e. InaccW -> ( ~P y ~< _om -> ~P y ~< x ) )
12 5 11 biimtrid 
 |-  ( x e. InaccW -> ( ~P y e. Fin -> ~P y ~< x ) )
13 4 12 biimtrid 
 |-  ( x e. InaccW -> ( y e. Fin -> ~P y ~< x ) )
14 13 ad3antlr 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> ( y e. Fin -> ~P y ~< x ) )
15 14 a1dd 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> ( y e. Fin -> ( y ~< z -> ~P y ~< x ) ) )
16 vex 
 |-  y e. _V
17 simplll 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> GCH = _V )
18 16 17 eleqtrrid 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> y e. GCH )
19 simprr 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> -. y e. Fin )
20 gchinf 
 |-  ( ( y e. GCH /\ -. y e. Fin ) -> _om ~<_ y )
21 18 19 20 syl2anc 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> _om ~<_ y )
22 vex 
 |-  z e. _V
23 22 17 eleqtrrid 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> z e. GCH )
24 gchpwdom 
 |-  ( ( _om ~<_ y /\ y e. GCH /\ z e. GCH ) -> ( y ~< z <-> ~P y ~<_ z ) )
25 21 18 23 24 syl3anc 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> ( y ~< z <-> ~P y ~<_ z ) )
26 winacard 
 |-  ( x e. InaccW -> ( card ` x ) = x )
27 iscard 
 |-  ( ( card ` x ) = x <-> ( x e. On /\ A. z e. x z ~< x ) )
28 27 simprbi 
 |-  ( ( card ` x ) = x -> A. z e. x z ~< x )
29 26 28 syl 
 |-  ( x e. InaccW -> A. z e. x z ~< x )
30 29 ad2antlr 
 |-  ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) -> A. z e. x z ~< x )
31 30 r19.21bi 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> z ~< x )
32 domsdomtr 
 |-  ( ( ~P y ~<_ z /\ z ~< x ) -> ~P y ~< x )
33 32 expcom 
 |-  ( z ~< x -> ( ~P y ~<_ z -> ~P y ~< x ) )
34 31 33 syl 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> ( ~P y ~<_ z -> ~P y ~< x ) )
35 34 adantrr 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> ( ~P y ~<_ z -> ~P y ~< x ) )
36 25 35 sylbid 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ ( z e. x /\ -. y e. Fin ) ) -> ( y ~< z -> ~P y ~< x ) )
37 36 expr 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> ( -. y e. Fin -> ( y ~< z -> ~P y ~< x ) ) )
38 15 37 pm2.61d 
 |-  ( ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) /\ z e. x ) -> ( y ~< z -> ~P y ~< x ) )
39 38 rexlimdva 
 |-  ( ( ( GCH = _V /\ x e. InaccW ) /\ y e. x ) -> ( E. z e. x y ~< z -> ~P y ~< x ) )
40 39 ralimdva 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> ( A. y e. x E. z e. x y ~< z -> A. y e. x ~P y ~< x ) )
41 2 3 40 3anim123d 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> ( ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) -> ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) ) )
42 elwina 
 |-  ( x e. InaccW <-> ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x E. z e. x y ~< z ) )
43 elina 
 |-  ( x e. Inacc <-> ( x =/= (/) /\ ( cf ` x ) = x /\ A. y e. x ~P y ~< x ) )
44 41 42 43 3imtr4g 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> ( x e. InaccW -> x e. Inacc ) )
45 1 44 mpd 
 |-  ( ( GCH = _V /\ x e. InaccW ) -> x e. Inacc )
46 45 ex 
 |-  ( GCH = _V -> ( x e. InaccW -> x e. Inacc ) )
47 inawina 
 |-  ( x e. Inacc -> x e. InaccW )
48 46 47 impbid1 
 |-  ( GCH = _V -> ( x e. InaccW <-> x e. Inacc ) )
49 48 eqrdv 
 |-  ( GCH = _V -> InaccW = Inacc )