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 ) |