This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wdom2d

Description: Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep ). (Contributed by Stefan O'Rear, 13-Feb-2015)

Ref Expression
Hypotheses wdom2d.a 
|- ( ph -> A e. V )
wdom2d.b 
|- ( ph -> B e. W )
wdom2d.o 
|- ( ( ph /\ x e. A ) -> E. y e. B x = X )
Assertion wdom2d 
|- ( ph -> A ~<_* B )

Proof

Step Hyp Ref Expression
1 wdom2d.a 
 |-  ( ph -> A e. V )
2 wdom2d.b 
 |-  ( ph -> B e. W )
3 wdom2d.o 
 |-  ( ( ph /\ x e. A ) -> E. y e. B x = X )
4 rabexg 
 |-  ( B e. W -> { z e. B | [_ z / y ]_ X e. A } e. _V )
5 2 4 syl 
 |-  ( ph -> { z e. B | [_ z / y ]_ X e. A } e. _V )
6 5 1 xpexd 
 |-  ( ph -> ( { z e. B | [_ z / y ]_ X e. A } X. A ) e. _V )
7 csbeq1 
 |-  ( z = w -> [_ z / y ]_ X = [_ w / y ]_ X )
8 7 eleq1d 
 |-  ( z = w -> ( [_ z / y ]_ X e. A <-> [_ w / y ]_ X e. A ) )
9 8 elrab 
 |-  ( w e. { z e. B | [_ z / y ]_ X e. A } <-> ( w e. B /\ [_ w / y ]_ X e. A ) )
10 9 simprbi 
 |-  ( w e. { z e. B | [_ z / y ]_ X e. A } -> [_ w / y ]_ X e. A )
11 10 adantl 
 |-  ( ( ph /\ w e. { z e. B | [_ z / y ]_ X e. A } ) -> [_ w / y ]_ X e. A )
12 11 fmpttd 
 |-  ( ph -> ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } --> A )
13 fssxp 
 |-  ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } --> A -> ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) C_ ( { z e. B | [_ z / y ]_ X e. A } X. A ) )
14 12 13 syl 
 |-  ( ph -> ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) C_ ( { z e. B | [_ z / y ]_ X e. A } X. A ) )
15 6 14 ssexd 
 |-  ( ph -> ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) e. _V )
16 eleq1 
 |-  ( x = X -> ( x e. A <-> X e. A ) )
17 16 biimpcd 
 |-  ( x e. A -> ( x = X -> X e. A ) )
18 17 ancrd 
 |-  ( x e. A -> ( x = X -> ( X e. A /\ x = X ) ) )
19 18 adantl 
 |-  ( ( ph /\ x e. A ) -> ( x = X -> ( X e. A /\ x = X ) ) )
20 19 reximdv 
 |-  ( ( ph /\ x e. A ) -> ( E. y e. B x = X -> E. y e. B ( X e. A /\ x = X ) ) )
21 3 20 mpd 
 |-  ( ( ph /\ x e. A ) -> E. y e. B ( X e. A /\ x = X ) )
22 nfv 
 |-  F/ v ( X e. A /\ x = X )
23 nfcsb1v 
 |-  F/_ y [_ v / y ]_ X
24 23 nfel1 
 |-  F/ y [_ v / y ]_ X e. A
25 23 nfeq2 
 |-  F/ y x = [_ v / y ]_ X
26 24 25 nfan 
 |-  F/ y ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X )
27 csbeq1a 
 |-  ( y = v -> X = [_ v / y ]_ X )
28 27 eleq1d 
 |-  ( y = v -> ( X e. A <-> [_ v / y ]_ X e. A ) )
29 27 eqeq2d 
 |-  ( y = v -> ( x = X <-> x = [_ v / y ]_ X ) )
30 28 29 anbi12d 
 |-  ( y = v -> ( ( X e. A /\ x = X ) <-> ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X ) ) )
31 22 26 30 cbvrexw 
 |-  ( E. y e. B ( X e. A /\ x = X ) <-> E. v e. B ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X ) )
32 21 31 sylib 
 |-  ( ( ph /\ x e. A ) -> E. v e. B ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X ) )
33 csbeq1 
 |-  ( z = v -> [_ z / y ]_ X = [_ v / y ]_ X )
34 33 eleq1d 
 |-  ( z = v -> ( [_ z / y ]_ X e. A <-> [_ v / y ]_ X e. A ) )
35 34 elrab 
 |-  ( v e. { z e. B | [_ z / y ]_ X e. A } <-> ( v e. B /\ [_ v / y ]_ X e. A ) )
36 35 simprbi 
 |-  ( v e. { z e. B | [_ z / y ]_ X e. A } -> [_ v / y ]_ X e. A )
37 csbeq1 
 |-  ( w = v -> [_ w / y ]_ X = [_ v / y ]_ X )
38 eqid 
 |-  ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) = ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X )
39 37 38 fvmptg 
 |-  ( ( v e. { z e. B | [_ z / y ]_ X e. A } /\ [_ v / y ]_ X e. A ) -> ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) = [_ v / y ]_ X )
40 36 39 mpdan 
 |-  ( v e. { z e. B | [_ z / y ]_ X e. A } -> ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) = [_ v / y ]_ X )
41 40 eqeq2d 
 |-  ( v e. { z e. B | [_ z / y ]_ X e. A } -> ( x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) <-> x = [_ v / y ]_ X ) )
42 41 rexbiia 
 |-  ( E. v e. { z e. B | [_ z / y ]_ X e. A } x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) <-> E. v e. { z e. B | [_ z / y ]_ X e. A } x = [_ v / y ]_ X )
43 34 rexrab 
 |-  ( E. v e. { z e. B | [_ z / y ]_ X e. A } x = [_ v / y ]_ X <-> E. v e. B ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X ) )
44 42 43 bitri 
 |-  ( E. v e. { z e. B | [_ z / y ]_ X e. A } x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) <-> E. v e. B ( [_ v / y ]_ X e. A /\ x = [_ v / y ]_ X ) )
45 32 44 sylibr 
 |-  ( ( ph /\ x e. A ) -> E. v e. { z e. B | [_ z / y ]_ X e. A } x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) )
46 45 ralrimiva 
 |-  ( ph -> A. x e. A E. v e. { z e. B | [_ z / y ]_ X e. A } x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) )
47 dffo3 
 |-  ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } -onto-> A <-> ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } --> A /\ A. x e. A E. v e. { z e. B | [_ z / y ]_ X e. A } x = ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) ` v ) ) )
48 12 46 47 sylanbrc 
 |-  ( ph -> ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } -onto-> A )
49 fowdom 
 |-  ( ( ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) e. _V /\ ( w e. { z e. B | [_ z / y ]_ X e. A } |-> [_ w / y ]_ X ) : { z e. B | [_ z / y ]_ X e. A } -onto-> A ) -> A ~<_* { z e. B | [_ z / y ]_ X e. A } )
50 15 48 49 syl2anc 
 |-  ( ph -> A ~<_* { z e. B | [_ z / y ]_ X e. A } )
51 ssrab2 
 |-  { z e. B | [_ z / y ]_ X e. A } C_ B
52 ssdomg 
 |-  ( B e. W -> ( { z e. B | [_ z / y ]_ X e. A } C_ B -> { z e. B | [_ z / y ]_ X e. A } ~<_ B ) )
53 51 52 mpi 
 |-  ( B e. W -> { z e. B | [_ z / y ]_ X e. A } ~<_ B )
54 domwdom 
 |-  ( { z e. B | [_ z / y ]_ X e. A } ~<_ B -> { z e. B | [_ z / y ]_ X e. A } ~<_* B )
55 2 53 54 3syl 
 |-  ( ph -> { z e. B | [_ z / y ]_ X e. A } ~<_* B )
56 wdomtr 
 |-  ( ( A ~<_* { z e. B | [_ z / y ]_ X e. A } /\ { z e. B | [_ z / y ]_ X e. A } ~<_* B ) -> A ~<_* B )
57 50 55 56 syl2anc 
 |-  ( ph -> A ~<_* B )