| Step |
Hyp |
Ref |
Expression |
| 1 |
|
sbthlem.1 |
|- A e. _V |
| 2 |
|
sbthlem.2 |
|- D = { x | ( x C_ A /\ ( g " ( B \ ( f " x ) ) ) C_ ( A \ x ) ) } |
| 3 |
|
sbthlem.3 |
|- H = ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) |
| 4 |
|
sbthlem.4 |
|- B e. _V |
| 5 |
4
|
brdom |
|- ( A ~<_ B <-> E. f f : A -1-1-> B ) |
| 6 |
1
|
brdom |
|- ( B ~<_ A <-> E. g g : B -1-1-> A ) |
| 7 |
5 6
|
anbi12i |
|- ( ( A ~<_ B /\ B ~<_ A ) <-> ( E. f f : A -1-1-> B /\ E. g g : B -1-1-> A ) ) |
| 8 |
|
exdistrv |
|- ( E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) <-> ( E. f f : A -1-1-> B /\ E. g g : B -1-1-> A ) ) |
| 9 |
7 8
|
bitr4i |
|- ( ( A ~<_ B /\ B ~<_ A ) <-> E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) ) |
| 10 |
|
vex |
|- f e. _V |
| 11 |
10
|
resex |
|- ( f |` U. D ) e. _V |
| 12 |
|
vex |
|- g e. _V |
| 13 |
12
|
cnvex |
|- `' g e. _V |
| 14 |
13
|
resex |
|- ( `' g |` ( A \ U. D ) ) e. _V |
| 15 |
11 14
|
unex |
|- ( ( f |` U. D ) u. ( `' g |` ( A \ U. D ) ) ) e. _V |
| 16 |
3 15
|
eqeltri |
|- H e. _V |
| 17 |
1 2 3
|
sbthlem9 |
|- ( ( f : A -1-1-> B /\ g : B -1-1-> A ) -> H : A -1-1-onto-> B ) |
| 18 |
|
f1oen3g |
|- ( ( H e. _V /\ H : A -1-1-onto-> B ) -> A ~~ B ) |
| 19 |
16 17 18
|
sylancr |
|- ( ( f : A -1-1-> B /\ g : B -1-1-> A ) -> A ~~ B ) |
| 20 |
19
|
exlimivv |
|- ( E. f E. g ( f : A -1-1-> B /\ g : B -1-1-> A ) -> A ~~ B ) |
| 21 |
9 20
|
sylbi |
|- ( ( A ~<_ B /\ B ~<_ A ) -> A ~~ B ) |