Step |
Hyp |
Ref |
Expression |
1 |
|
dfac10 |
⊢ ( CHOICE ↔ dom card = V ) |
2 |
|
basfn |
⊢ Base Fn V |
3 |
|
ssv |
⊢ Grp ⊆ V |
4 |
|
fvelimab |
⊢ ( ( Base Fn V ∧ Grp ⊆ V ) → ( 𝑥 ∈ ( Base “ Grp ) ↔ ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 ) ) |
5 |
2 3 4
|
mp2an |
⊢ ( 𝑥 ∈ ( Base “ Grp ) ↔ ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 ) |
7 |
6
|
grpbn0 |
⊢ ( 𝑦 ∈ Grp → ( Base ‘ 𝑦 ) ≠ ∅ ) |
8 |
|
neeq1 |
⊢ ( ( Base ‘ 𝑦 ) = 𝑥 → ( ( Base ‘ 𝑦 ) ≠ ∅ ↔ 𝑥 ≠ ∅ ) ) |
9 |
7 8
|
syl5ibcom |
⊢ ( 𝑦 ∈ Grp → ( ( Base ‘ 𝑦 ) = 𝑥 → 𝑥 ≠ ∅ ) ) |
10 |
9
|
rexlimiv |
⊢ ( ∃ 𝑦 ∈ Grp ( Base ‘ 𝑦 ) = 𝑥 → 𝑥 ≠ ∅ ) |
11 |
5 10
|
sylbi |
⊢ ( 𝑥 ∈ ( Base “ Grp ) → 𝑥 ≠ ∅ ) |
12 |
11
|
adantl |
⊢ ( ( dom card = V ∧ 𝑥 ∈ ( Base “ Grp ) ) → 𝑥 ≠ ∅ ) |
13 |
|
vex |
⊢ 𝑥 ∈ V |
14 |
12 13
|
jctil |
⊢ ( ( dom card = V ∧ 𝑥 ∈ ( Base “ Grp ) ) → ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) |
15 |
|
ablgrp |
⊢ ( 𝑥 ∈ Abel → 𝑥 ∈ Grp ) |
16 |
15
|
ssriv |
⊢ Abel ⊆ Grp |
17 |
|
imass2 |
⊢ ( Abel ⊆ Grp → ( Base “ Abel ) ⊆ ( Base “ Grp ) ) |
18 |
16 17
|
ax-mp |
⊢ ( Base “ Abel ) ⊆ ( Base “ Grp ) |
19 |
|
simprl |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ V ) |
20 |
|
simpl |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → dom card = V ) |
21 |
19 20
|
eleqtrrd |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ dom card ) |
22 |
|
simprr |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ≠ ∅ ) |
23 |
|
isnumbasgrplem3 |
⊢ ( ( 𝑥 ∈ dom card ∧ 𝑥 ≠ ∅ ) → 𝑥 ∈ ( Base “ Abel ) ) |
24 |
21 22 23
|
syl2anc |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( Base “ Abel ) ) |
25 |
18 24
|
sseldi |
⊢ ( ( dom card = V ∧ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) → 𝑥 ∈ ( Base “ Grp ) ) |
26 |
14 25
|
impbida |
⊢ ( dom card = V → ( 𝑥 ∈ ( Base “ Grp ) ↔ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) ) |
27 |
|
eldifsn |
⊢ ( 𝑥 ∈ ( V ∖ { ∅ } ) ↔ ( 𝑥 ∈ V ∧ 𝑥 ≠ ∅ ) ) |
28 |
26 27
|
bitr4di |
⊢ ( dom card = V → ( 𝑥 ∈ ( Base “ Grp ) ↔ 𝑥 ∈ ( V ∖ { ∅ } ) ) ) |
29 |
28
|
eqrdv |
⊢ ( dom card = V → ( Base “ Grp ) = ( V ∖ { ∅ } ) ) |
30 |
|
fvex |
⊢ ( har ‘ 𝑥 ) ∈ V |
31 |
13 30
|
unex |
⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ V |
32 |
|
ssun2 |
⊢ ( har ‘ 𝑥 ) ⊆ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) |
33 |
|
harn0 |
⊢ ( 𝑥 ∈ V → ( har ‘ 𝑥 ) ≠ ∅ ) |
34 |
13 33
|
ax-mp |
⊢ ( har ‘ 𝑥 ) ≠ ∅ |
35 |
|
ssn0 |
⊢ ( ( ( har ‘ 𝑥 ) ⊆ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∧ ( har ‘ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅ ) |
36 |
32 34 35
|
mp2an |
⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅ |
37 |
|
eldifsn |
⊢ ( ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } ) ↔ ( ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ V ∧ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ≠ ∅ ) ) |
38 |
31 36 37
|
mpbir2an |
⊢ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } ) |
39 |
38
|
a1i |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( V ∖ { ∅ } ) ) |
40 |
|
id |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( Base “ Grp ) = ( V ∖ { ∅ } ) ) |
41 |
39 40
|
eleqtrrd |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( Base “ Grp ) ) |
42 |
|
isnumbasgrp |
⊢ ( 𝑥 ∈ dom card ↔ ( 𝑥 ∪ ( har ‘ 𝑥 ) ) ∈ ( Base “ Grp ) ) |
43 |
41 42
|
sylibr |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → 𝑥 ∈ dom card ) |
44 |
13
|
a1i |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → 𝑥 ∈ V ) |
45 |
43 44
|
2thd |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → ( 𝑥 ∈ dom card ↔ 𝑥 ∈ V ) ) |
46 |
45
|
eqrdv |
⊢ ( ( Base “ Grp ) = ( V ∖ { ∅ } ) → dom card = V ) |
47 |
29 46
|
impbii |
⊢ ( dom card = V ↔ ( Base “ Grp ) = ( V ∖ { ∅ } ) ) |
48 |
1 47
|
bitri |
⊢ ( CHOICE ↔ ( Base “ Grp ) = ( V ∖ { ∅ } ) ) |