Step |
Hyp |
Ref |
Expression |
1 |
|
simpl |
|- ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> R We A ) |
2 |
|
vex |
|- f e. _V |
3 |
|
isof1o |
|- ( f Isom R , S ( A , B ) -> f : A -1-1-onto-> B ) |
4 |
|
f1of |
|- ( f : A -1-1-onto-> B -> f : A --> B ) |
5 |
3 4
|
syl |
|- ( f Isom R , S ( A , B ) -> f : A --> B ) |
6 |
|
dmfex |
|- ( ( f e. _V /\ f : A --> B ) -> A e. _V ) |
7 |
2 5 6
|
sylancr |
|- ( f Isom R , S ( A , B ) -> A e. _V ) |
8 |
7
|
ad2antrl |
|- ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> A e. _V ) |
9 |
|
exse |
|- ( A e. _V -> R Se A ) |
10 |
8 9
|
syl |
|- ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> R Se A ) |
11 |
1 10
|
jca |
|- ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> ( R We A /\ R Se A ) ) |
12 |
|
weisoeq |
|- ( ( ( R We A /\ R Se A ) /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> f = g ) |
13 |
11 12
|
sylancom |
|- ( ( R We A /\ ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) ) -> f = g ) |
14 |
13
|
ex |
|- ( R We A -> ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) ) |
15 |
14
|
alrimivv |
|- ( R We A -> A. f A. g ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) ) |
16 |
|
isoeq1 |
|- ( f = g -> ( f Isom R , S ( A , B ) <-> g Isom R , S ( A , B ) ) ) |
17 |
16
|
mo4 |
|- ( E* f f Isom R , S ( A , B ) <-> A. f A. g ( ( f Isom R , S ( A , B ) /\ g Isom R , S ( A , B ) ) -> f = g ) ) |
18 |
15 17
|
sylibr |
|- ( R We A -> E* f f Isom R , S ( A , B ) ) |