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