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 ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) → 𝑆 ∈ dom card )

Proof

Step Hyp Ref Expression
1 basfn ⊢ Base Fn V
2 ssv ⊢ Grp ⊆ V
3 fvelimab ⊢ ( ( Base Fn V ∧ Grp ⊆ V ) → ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) ↔ ∃ 𝑥 ∈ Grp ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) )
4 1 2 3 mp2an ⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) ↔ ∃ 𝑥 ∈ Grp ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) )
5 harcl ⊢ ( har ‘ 𝑆 ) ∈ On
6 onenon ⊢ ( ( har ‘ 𝑆 ) ∈ On → ( har ‘ 𝑆 ) ∈ dom card )
7 5 6 ax-mp ⊢ ( har ‘ 𝑆 ) ∈ dom card
8 xpnum ⊢ ( ( ( har ‘ 𝑆 ) ∈ dom card ∧ ( har ‘ 𝑆 ) ∈ dom card ) → ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ∈ dom card )
9 7 7 8 mp2an ⊢ ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ∈ dom card
10 ssun1 ⊢ 𝑆 ⊆ ( 𝑆 ∪ ( har ‘ 𝑆 ) )
11 simpr ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) )
12 10 11 sseqtrrid ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑥 ) )
13 fvex ⊢ ( Base ‘ 𝑥 ) ∈ V
14 13 ssex ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑥 ) → 𝑆 ∈ V )
15 12 14 syl ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → 𝑆 ∈ V )
16 7 a1i ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → ( har ‘ 𝑆 ) ∈ dom card )
17 simp1l ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑥 ∈ Grp )
18 12 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝑥 ) )
19 simp2 ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑎 ∈ 𝑆 )
20 18 19 sseldd ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑎 ∈ ( Base ‘ 𝑥 ) )
21 ssun2 ⊢ ( har ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( har ‘ 𝑆 ) )
22 21 11 sseqtrrid ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → ( har ‘ 𝑆 ) ⊆ ( Base ‘ 𝑥 ) )
23 22 3ad2ant1 ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → ( har ‘ 𝑆 ) ⊆ ( Base ‘ 𝑥 ) )
24 simp3 ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑐 ∈ ( har ‘ 𝑆 ) )
25 23 24 sseldd ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → 𝑐 ∈ ( Base ‘ 𝑥 ) )
26 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
27 eqid ⊢ ( +g ‘ 𝑥 ) = ( +g ‘ 𝑥 )
28 26 27 grpcl ⊢ ( ( 𝑥 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑥 ) ∧ 𝑐 ∈ ( Base ‘ 𝑥 ) ) → ( 𝑎 ( +g ‘ 𝑥 ) 𝑐 ) ∈ ( Base ‘ 𝑥 ) )
29 17 20 25 28 syl3anc ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → ( 𝑎 ( +g ‘ 𝑥 ) 𝑐 ) ∈ ( Base ‘ 𝑥 ) )
30 simp1r ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) )
31 29 30 eleqtrd ⊢ ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ∧ 𝑐 ∈ ( har ‘ 𝑆 ) ) → ( 𝑎 ( +g ‘ 𝑥 ) 𝑐 ) ∈ ( 𝑆 ∪ ( har ‘ 𝑆 ) ) )
32 simplll ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑥 ∈ Grp )
33 22 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → ( har ‘ 𝑆 ) ⊆ ( Base ‘ 𝑥 ) )
34 simprl ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑐 ∈ ( har ‘ 𝑆 ) )
35 33 34 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑐 ∈ ( Base ‘ 𝑥 ) )
36 simprr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑑 ∈ ( har ‘ 𝑆 ) )
37 33 36 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑑 ∈ ( Base ‘ 𝑥 ) )
38 12 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑆 ⊆ ( Base ‘ 𝑥 ) )
39 simplr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑎 ∈ 𝑆 )
40 38 39 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → 𝑎 ∈ ( Base ‘ 𝑥 ) )
41 26 27 grplcan ⊢ ( ( 𝑥 ∈ Grp ∧ ( 𝑐 ∈ ( Base ‘ 𝑥 ) ∧ 𝑑 ∈ ( Base ‘ 𝑥 ) ∧ 𝑎 ∈ ( Base ‘ 𝑥 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑥 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑥 ) 𝑑 ) ↔ 𝑐 = 𝑑 ) )
42 32 35 37 40 41 syl13anc ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑎 ∈ 𝑆 ) ∧ ( 𝑐 ∈ ( har ‘ 𝑆 ) ∧ 𝑑 ∈ ( har ‘ 𝑆 ) ) ) → ( ( 𝑎 ( +g ‘ 𝑥 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑥 ) 𝑑 ) ↔ 𝑐 = 𝑑 ) )
43 simplll ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑥 ∈ Grp )
44 12 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝑥 ) )
45 simprr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑑 ∈ 𝑆 )
46 44 45 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑑 ∈ ( Base ‘ 𝑥 ) )
47 simprl ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑎 ∈ 𝑆 )
48 44 47 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑎 ∈ ( Base ‘ 𝑥 ) )
49 22 ad2antrr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( har ‘ 𝑆 ) ⊆ ( Base ‘ 𝑥 ) )
50 simplr ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑏 ∈ ( har ‘ 𝑆 ) )
51 49 50 sseldd ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → 𝑏 ∈ ( Base ‘ 𝑥 ) )
52 26 27 grprcan ⊢ ( ( 𝑥 ∈ Grp ∧ ( 𝑑 ∈ ( Base ‘ 𝑥 ) ∧ 𝑎 ∈ ( Base ‘ 𝑥 ) ∧ 𝑏 ∈ ( Base ‘ 𝑥 ) ) ) → ( ( 𝑑 ( +g ‘ 𝑥 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑥 ) 𝑏 ) ↔ 𝑑 = 𝑎 ) )
53 43 46 48 51 52 syl13anc ⊢ ( ( ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) ∧ 𝑏 ∈ ( har ‘ 𝑆 ) ) ∧ ( 𝑎 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆 ) ) → ( ( 𝑑 ( +g ‘ 𝑥 ) 𝑏 ) = ( 𝑎 ( +g ‘ 𝑥 ) 𝑏 ) ↔ 𝑑 = 𝑎 ) )
54 harndom ⊢ ¬ ( har ‘ 𝑆 ) ≼ 𝑆
55 54 a1i ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → ¬ ( har ‘ 𝑆 ) ≼ 𝑆 )
56 15 16 16 31 42 53 55 unxpwdom3 ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → 𝑆 ≼* ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) )
57 wdomnumr ⊢ ( ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ∈ dom card → ( 𝑆 ≼* ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ↔ 𝑆 ≼ ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ) )
58 9 57 ax-mp ⊢ ( 𝑆 ≼* ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ↔ 𝑆 ≼ ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) )
59 56 58 sylib ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → 𝑆 ≼ ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) )
60 numdom ⊢ ( ( ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ∈ dom card ∧ 𝑆 ≼ ( ( har ‘ 𝑆 ) × ( har ‘ 𝑆 ) ) ) → 𝑆 ∈ dom card )
61 9 59 60 sylancr ⊢ ( ( 𝑥 ∈ Grp ∧ ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ) → 𝑆 ∈ dom card )
62 61 rexlimiva ⊢ ( ∃ 𝑥 ∈ Grp ( Base ‘ 𝑥 ) = ( 𝑆 ∪ ( har ‘ 𝑆 ) ) → 𝑆 ∈ dom card )
63 4 62 sylbi ⊢ ( ( 𝑆 ∪ ( har ‘ 𝑆 ) ) ∈ ( Base “ Grp ) → 𝑆 ∈ dom card )