Metamath Proof Explorer

Theorem isnumbasgrplem2

Description: If the (to be thought of as disjoint, although the proof does not require this) union of a set and its Hartogs number supports a group structure (more generally, a cancellative magma), then the set must be numerable. (Contributed by Stefan O'Rear, 9-Jul-2015)

Ref Expression
Assertion isnumbasgrplem2 
|- ( ( S u. ( har ` S ) ) e. ( Base " Grp ) -> S e. dom card )

Proof

Step Hyp Ref Expression
1 basfn 
 |-  Base Fn _V
2 ssv 
 |-  Grp C_ _V
3 fvelimab 
 |-  ( ( Base Fn _V /\ Grp C_ _V ) -> ( ( S u. ( har ` S ) ) e. ( Base " Grp ) <-> E. x e. Grp ( Base ` x ) = ( S u. ( har ` S ) ) ) )
4 1 2 3 mp2an 
 |-  ( ( S u. ( har ` S ) ) e. ( Base " Grp ) <-> E. x e. Grp ( Base ` x ) = ( S u. ( har ` S ) ) )
5 harcl 
 |-  ( har ` S ) e. On
6 onenon 
 |-  ( ( har ` S ) e. On -> ( har ` S ) e. dom card )
7 5 6 ax-mp 
 |-  ( har ` S ) e. dom card
8 xpnum 
 |-  ( ( ( har ` S ) e. dom card /\ ( har ` S ) e. dom card ) -> ( ( har ` S ) X. ( har ` S ) ) e. dom card )
9 7 7 8 mp2an 
 |-  ( ( har ` S ) X. ( har ` S ) ) e. dom card
10 ssun1 
 |-  S C_ ( S u. ( har ` S ) )
11 simpr 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> ( Base ` x ) = ( S u. ( har ` S ) ) )
12 10 11 sseqtrrid 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> S C_ ( Base ` x ) )
13 fvex 
 |-  ( Base ` x ) e. _V
14 13 ssex 
 |-  ( S C_ ( Base ` x ) -> S e. _V )
15 12 14 syl 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> S e. _V )
16 7 a1i 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> ( har ` S ) e. dom card )
17 simp1l 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> x e. Grp )
18 12 3ad2ant1 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> S C_ ( Base ` x ) )
19 simp2 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> a e. S )
20 18 19 sseldd 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> a e. ( Base ` x ) )
21 ssun2 
 |-  ( har ` S ) C_ ( S u. ( har ` S ) )
22 21 11 sseqtrrid 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> ( har ` S ) C_ ( Base ` x ) )
23 22 3ad2ant1 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> ( har ` S ) C_ ( Base ` x ) )
24 simp3 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> c e. ( har ` S ) )
25 23 24 sseldd 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> c e. ( Base ` x ) )
26 eqid 
 |-  ( Base ` x ) = ( Base ` x )
27 eqid 
 |-  ( +g ` x ) = ( +g ` x )
28 26 27 grpcl 
 |-  ( ( x e. Grp /\ a e. ( Base ` x ) /\ c e. ( Base ` x ) ) -> ( a ( +g ` x ) c ) e. ( Base ` x ) )
29 17 20 25 28 syl3anc 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> ( a ( +g ` x ) c ) e. ( Base ` x ) )
30 simp1r 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> ( Base ` x ) = ( S u. ( har ` S ) ) )
31 29 30 eleqtrd 
 |-  ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S /\ c e. ( har ` S ) ) -> ( a ( +g ` x ) c ) e. ( S u. ( har ` S ) ) )
32 simplll 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> x e. Grp )
33 22 ad2antrr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> ( har ` S ) C_ ( Base ` x ) )
34 simprl 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> c e. ( har ` S ) )
35 33 34 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> c e. ( Base ` x ) )
36 simprr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> d e. ( har ` S ) )
37 33 36 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> d e. ( Base ` x ) )
38 12 ad2antrr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> S C_ ( Base ` x ) )
39 simplr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> a e. S )
40 38 39 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> a e. ( Base ` x ) )
41 26 27 grplcan 
 |-  ( ( x e. Grp /\ ( c e. ( Base ` x ) /\ d e. ( Base ` x ) /\ a e. ( Base ` x ) ) ) -> ( ( a ( +g ` x ) c ) = ( a ( +g ` x ) d ) <-> c = d ) )
42 32 35 37 40 41 syl13anc 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ a e. S ) /\ ( c e. ( har ` S ) /\ d e. ( har ` S ) ) ) -> ( ( a ( +g ` x ) c ) = ( a ( +g ` x ) d ) <-> c = d ) )
43 simplll 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> x e. Grp )
44 12 ad2antrr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> S C_ ( Base ` x ) )
45 simprr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> d e. S )
46 44 45 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> d e. ( Base ` x ) )
47 simprl 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> a e. S )
48 44 47 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> a e. ( Base ` x ) )
49 22 ad2antrr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> ( har ` S ) C_ ( Base ` x ) )
50 simplr 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> b e. ( har ` S ) )
51 49 50 sseldd 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> b e. ( Base ` x ) )
52 26 27 grprcan 
 |-  ( ( x e. Grp /\ ( d e. ( Base ` x ) /\ a e. ( Base ` x ) /\ b e. ( Base ` x ) ) ) -> ( ( d ( +g ` x ) b ) = ( a ( +g ` x ) b ) <-> d = a ) )
53 43 46 48 51 52 syl13anc 
 |-  ( ( ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) /\ b e. ( har ` S ) ) /\ ( a e. S /\ d e. S ) ) -> ( ( d ( +g ` x ) b ) = ( a ( +g ` x ) b ) <-> d = a ) )
54 harndom 
 |-  -. ( har ` S ) ~<_ S
55 54 a1i 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> -. ( har ` S ) ~<_ S )
56 15 16 16 31 42 53 55 unxpwdom3 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> S ~<_* ( ( har ` S ) X. ( har ` S ) ) )
57 wdomnumr 
 |-  ( ( ( har ` S ) X. ( har ` S ) ) e. dom card -> ( S ~<_* ( ( har ` S ) X. ( har ` S ) ) <-> S ~<_ ( ( har ` S ) X. ( har ` S ) ) ) )
58 9 57 ax-mp 
 |-  ( S ~<_* ( ( har ` S ) X. ( har ` S ) ) <-> S ~<_ ( ( har ` S ) X. ( har ` S ) ) )
59 56 58 sylib 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> S ~<_ ( ( har ` S ) X. ( har ` S ) ) )
60 numdom 
 |-  ( ( ( ( har ` S ) X. ( har ` S ) ) e. dom card /\ S ~<_ ( ( har ` S ) X. ( har ` S ) ) ) -> S e. dom card )
61 9 59 60 sylancr 
 |-  ( ( x e. Grp /\ ( Base ` x ) = ( S u. ( har ` S ) ) ) -> S e. dom card )
62 61 rexlimiva 
 |-  ( E. x e. Grp ( Base ` x ) = ( S u. ( har ` S ) ) -> S e. dom card )
63 4 62 sylbi 
 |-  ( ( S u. ( har ` S ) ) e. ( Base " Grp ) -> S e. dom card )