Step |
Hyp |
Ref |
Expression |
1 |
|
rabfodom.1 |
|- ( ( ph /\ x e. A /\ y = ( F ` x ) ) -> ( ch <-> ps ) ) |
2 |
|
rabfodom.2 |
|- ( ph -> A e. V ) |
3 |
|
rabfodom.3 |
|- ( ph -> F : A -onto-> B ) |
4 |
|
vex |
|- a e. _V |
5 |
4
|
rabex |
|- { x e. a | ps } e. _V |
6 |
|
eqid |
|- ( x e. a |-> ( F ` x ) ) = ( x e. a |-> ( F ` x ) ) |
7 |
|
fof |
|- ( F : A -onto-> B -> F : A --> B ) |
8 |
3 7
|
syl |
|- ( ph -> F : A --> B ) |
9 |
8
|
feqmptd |
|- ( ph -> F = ( x e. A |-> ( F ` x ) ) ) |
10 |
9
|
ad2antrr |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> F = ( x e. A |-> ( F ` x ) ) ) |
11 |
10
|
reseq1d |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( F |` a ) = ( ( x e. A |-> ( F ` x ) ) |` a ) ) |
12 |
|
elpwi |
|- ( a e. ~P A -> a C_ A ) |
13 |
12
|
ad2antlr |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> a C_ A ) |
14 |
13
|
resmptd |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( ( x e. A |-> ( F ` x ) ) |` a ) = ( x e. a |-> ( F ` x ) ) ) |
15 |
11 14
|
eqtrd |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( F |` a ) = ( x e. a |-> ( F ` x ) ) ) |
16 |
|
f1oeq1 |
|- ( ( F |` a ) = ( x e. a |-> ( F ` x ) ) -> ( ( F |` a ) : a -1-1-onto-> B <-> ( x e. a |-> ( F ` x ) ) : a -1-1-onto-> B ) ) |
17 |
16
|
biimpa |
|- ( ( ( F |` a ) = ( x e. a |-> ( F ` x ) ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( x e. a |-> ( F ` x ) ) : a -1-1-onto-> B ) |
18 |
15 17
|
sylancom |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( x e. a |-> ( F ` x ) ) : a -1-1-onto-> B ) |
19 |
|
simp1ll |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> ph ) |
20 |
13
|
3ad2ant1 |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> a C_ A ) |
21 |
|
simp2 |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> x e. a ) |
22 |
20 21
|
sseldd |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> x e. A ) |
23 |
|
simp3 |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> y = ( F ` x ) ) |
24 |
19 22 23 1
|
syl3anc |
|- ( ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) /\ x e. a /\ y = ( F ` x ) ) -> ( ch <-> ps ) ) |
25 |
6 18 24
|
f1oresrab |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> ( ( x e. a |-> ( F ` x ) ) |` { x e. a | ps } ) : { x e. a | ps } -1-1-onto-> { y e. B | ch } ) |
26 |
|
f1oeng |
|- ( ( { x e. a | ps } e. _V /\ ( ( x e. a |-> ( F ` x ) ) |` { x e. a | ps } ) : { x e. a | ps } -1-1-onto-> { y e. B | ch } ) -> { x e. a | ps } ~~ { y e. B | ch } ) |
27 |
5 25 26
|
sylancr |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { x e. a | ps } ~~ { y e. B | ch } ) |
28 |
27
|
ensymd |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { y e. B | ch } ~~ { x e. a | ps } ) |
29 |
|
rabexg |
|- ( A e. V -> { x e. A | ps } e. _V ) |
30 |
2 29
|
syl |
|- ( ph -> { x e. A | ps } e. _V ) |
31 |
30
|
ad2antrr |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { x e. A | ps } e. _V ) |
32 |
|
rabss2 |
|- ( a C_ A -> { x e. a | ps } C_ { x e. A | ps } ) |
33 |
13 32
|
syl |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { x e. a | ps } C_ { x e. A | ps } ) |
34 |
|
ssdomg |
|- ( { x e. A | ps } e. _V -> ( { x e. a | ps } C_ { x e. A | ps } -> { x e. a | ps } ~<_ { x e. A | ps } ) ) |
35 |
31 33 34
|
sylc |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { x e. a | ps } ~<_ { x e. A | ps } ) |
36 |
|
endomtr |
|- ( ( { y e. B | ch } ~~ { x e. a | ps } /\ { x e. a | ps } ~<_ { x e. A | ps } ) -> { y e. B | ch } ~<_ { x e. A | ps } ) |
37 |
28 35 36
|
syl2anc |
|- ( ( ( ph /\ a e. ~P A ) /\ ( F |` a ) : a -1-1-onto-> B ) -> { y e. B | ch } ~<_ { x e. A | ps } ) |
38 |
|
foresf1o |
|- ( ( A e. V /\ F : A -onto-> B ) -> E. a e. ~P A ( F |` a ) : a -1-1-onto-> B ) |
39 |
2 3 38
|
syl2anc |
|- ( ph -> E. a e. ~P A ( F |` a ) : a -1-1-onto-> B ) |
40 |
37 39
|
r19.29a |
|- ( ph -> { y e. B | ch } ~<_ { x e. A | ps } ) |