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 )