Metamath Proof Explorer


Theorem rabfodom

Description: Domination relation for restricted abstract class builders, based on a surjective function. (Contributed by Thierry Arnoux, 27-Jan-2020)

Ref Expression
Hypotheses rabfodom.1
|- ( ( ph /\ x e. A /\ y = ( F ` x ) ) -> ( ch <-> ps ) )
rabfodom.2
|- ( ph -> A e. V )
rabfodom.3
|- ( ph -> F : A -onto-> B )
Assertion rabfodom
|- ( ph -> { y e. B | ch } ~<_ { x e. A | ps } )

Proof

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 } )