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 )