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 \cup har (S) \in Base [Grp] \to S \in dom card$

Proof

Step	Hyp	Ref	Expression
1		basfn	$⊢ Base Fn V$
2		ssv	$⊢ Grp \subseteq V$
3		fvelimab	$⊢ (Base Fn V \land Grp \subseteq V) \to (S \cup har (S) \in Base [Grp] \leftrightarrow \exists x \in Grp {Base}_{x} = S \cup har (S))$
4	1 2 3	mp2an	$⊢ S \cup har (S) \in Base [Grp] \leftrightarrow \exists x \in Grp {Base}_{x} = S \cup har (S)$
5		harcl	$⊢ har (S) \in On$
6		onenon	$⊢ har (S) \in On \to har (S) \in dom card$
7	5 6	ax-mp	$⊢ har (S) \in dom card$
8		xpnum	$⊢ (har (S) \in dom card \land har (S) \in dom card) \to har (S) \times har (S) \in dom card$
9	7 7 8	mp2an	$⊢ har (S) \times har (S) \in dom card$
10		ssun1	$⊢ S \subseteq S \cup har (S)$
11		simpr	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to {Base}_{x} = S \cup har (S)$
12	10 11	sseqtrrid	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to S \subseteq {Base}_{x}$
13		fvex	$⊢ {Base}_{x} \in V$
14	13	ssex	$⊢ S \subseteq {Base}_{x} \to S \in V$
15	12 14	syl	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to S \in V$
16	7	a1i	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to har (S) \in dom card$
17		simp1l	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to x \in Grp$
18	12	3ad2ant1	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to S \subseteq {Base}_{x}$
19		simp2	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to a \in S$
20	18 19	sseldd	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to a \in {Base}_{x}$
21		ssun2	$⊢ har (S) \subseteq S \cup har (S)$
22	21 11	sseqtrrid	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to har (S) \subseteq {Base}_{x}$
23	22	3ad2ant1	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to har (S) \subseteq {Base}_{x}$
24		simp3	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to c \in har (S)$
25	23 24	sseldd	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to c \in {Base}_{x}$
26		eqid	$⊢ {Base}_{x} = {Base}_{x}$
27		eqid	$⊢ +_{x} = +_{x}$
28	26 27	grpcl	$⊢ (x \in Grp \land a \in {Base}_{x} \land c \in {Base}_{x}) \to a +_{x} c \in {Base}_{x}$
29	17 20 25 28	syl3anc	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to a +_{x} c \in {Base}_{x}$
30		simp1r	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to {Base}_{x} = S \cup har (S)$
31	29 30	eleqtrd	$⊢ ((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S \land c \in har (S)) \to a +_{x} c \in (S \cup har (S))$
32		simplll	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to x \in Grp$
33	22	ad2antrr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to har (S) \subseteq {Base}_{x}$
34		simprl	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to c \in har (S)$
35	33 34	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to c \in {Base}_{x}$
36		simprr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to d \in har (S)$
37	33 36	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to d \in {Base}_{x}$
38	12	ad2antrr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to S \subseteq {Base}_{x}$
39		simplr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to a \in S$
40	38 39	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to a \in {Base}_{x}$
41	26 27	grplcan	$⊢ (x \in Grp \land (c \in {Base}_{x} \land d \in {Base}_{x} \land a \in {Base}_{x})) \to (a +_{x} c = a +_{x} d \leftrightarrow c = d)$
42	32 35 37 40 41	syl13anc	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land a \in S) \land (c \in har (S) \land d \in har (S))) \to (a +_{x} c = a +_{x} d \leftrightarrow c = d)$
43		simplll	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to x \in Grp$
44	12	ad2antrr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to S \subseteq {Base}_{x}$
45		simprr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to d \in S$
46	44 45	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to d \in {Base}_{x}$
47		simprl	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to a \in S$
48	44 47	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to a \in {Base}_{x}$
49	22	ad2antrr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to har (S) \subseteq {Base}_{x}$
50		simplr	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to b \in har (S)$
51	49 50	sseldd	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to b \in {Base}_{x}$
52	26 27	grprcan	$⊢ (x \in Grp \land (d \in {Base}_{x} \land a \in {Base}_{x} \land b \in {Base}_{x})) \to (d +_{x} b = a +_{x} b \leftrightarrow d = a)$
53	43 46 48 51 52	syl13anc	$⊢ (((x \in Grp \land {Base}_{x} = S \cup har (S)) \land b \in har (S)) \land (a \in S \land d \in S)) \to (d +_{x} b = a +_{x} b \leftrightarrow d = a)$
54		harndom	$⊢ \neg har (S) ≼ S$
55	54	a1i	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to \neg har (S) ≼ S$
56	15 16 16 31 42 53 55	unxpwdom3	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to S ≼^{*} (har (S) \times har (S))$
57		wdomnumr	$⊢ har (S) \times har (S) \in dom card \to (S ≼^{*} (har (S) \times har (S)) \leftrightarrow S ≼ (har (S) \times har (S)))$
58	9 57	ax-mp	$⊢ S ≼^{*} (har (S) \times har (S)) \leftrightarrow S ≼ (har (S) \times har (S))$
59	56 58	sylib	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to S ≼ (har (S) \times har (S))$
60		numdom	$⊢ (har (S) \times har (S) \in dom card \land S ≼ (har (S) \times har (S))) \to S \in dom card$
61	9 59 60	sylancr	$⊢ (x \in Grp \land {Base}_{x} = S \cup har (S)) \to S \in dom card$
62	61	rexlimiva	$⊢ \exists x \in Grp {Base}_{x} = S \cup har (S) \to S \in dom card$
63	4 62	sylbi	$⊢ S \cup har (S) \in Base [Grp] \to S \in dom card$

Metamath Proof Explorer

Theorem isnumbasgrplem2

Proof