Step |
Hyp |
Ref |
Expression |
1 |
|
ssequn2 |
|- ( ( _V \ dom card ) C_ Fin <-> ( Fin u. ( _V \ dom card ) ) = Fin ) |
2 |
|
dfac10 |
|- ( CHOICE <-> dom card = _V ) |
3 |
|
finnum |
|- ( x e. Fin -> x e. dom card ) |
4 |
3
|
ssriv |
|- Fin C_ dom card |
5 |
|
ssequn2 |
|- ( Fin C_ dom card <-> ( dom card u. Fin ) = dom card ) |
6 |
4 5
|
mpbi |
|- ( dom card u. Fin ) = dom card |
7 |
6
|
eqeq1i |
|- ( ( dom card u. Fin ) = _V <-> dom card = _V ) |
8 |
2 7
|
bitr4i |
|- ( CHOICE <-> ( dom card u. Fin ) = _V ) |
9 |
|
ssv |
|- ( dom card u. Fin ) C_ _V |
10 |
|
eqss |
|- ( ( dom card u. Fin ) = _V <-> ( ( dom card u. Fin ) C_ _V /\ _V C_ ( dom card u. Fin ) ) ) |
11 |
9 10
|
mpbiran |
|- ( ( dom card u. Fin ) = _V <-> _V C_ ( dom card u. Fin ) ) |
12 |
|
ssundif |
|- ( _V C_ ( dom card u. Fin ) <-> ( _V \ dom card ) C_ Fin ) |
13 |
8 11 12
|
3bitri |
|- ( CHOICE <-> ( _V \ dom card ) C_ Fin ) |
14 |
|
dffin7-2 |
|- Fin7 = ( Fin u. ( _V \ dom card ) ) |
15 |
14
|
eqeq1i |
|- ( Fin7 = Fin <-> ( Fin u. ( _V \ dom card ) ) = Fin ) |
16 |
1 13 15
|
3bitr4i |
|- ( CHOICE <-> Fin7 = Fin ) |