Theorem wdom2d2

Description: Deduction for weak dominance by a Cartesian product.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015)

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

Proof

Step	Hyp	Ref	Expression
1		wdom2d2.a	|- ( ph -> A e. V )
2		wdom2d2.b	|- ( ph -> B e. W )
3		wdom2d2.c	|- ( ph -> C e. X )
4		wdom2d2.o	|- ( ( ph /\ x e. A ) -> E. y e. B E. z e. C x = X )
5	2 3	xpexd	|- ( ph -> ( B X. C ) e. _V )
6		nfcsb1v	|- F/_ y [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X
7	6	nfeq2	|- F/ y x = [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X
8		nfcv	|- F/_ z ( 1st ` w )
9		nfcsb1v	|- F/_ z [_ ( 2nd ` w ) / z ]_ X
10	8 9	nfcsbw	|- F/_ z [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X
11	10	nfeq2	|- F/ z x = [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X
12		nfv	|- F/ w x = X
13		csbopeq1a	|- ( w = <. y , z >. -> [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X = X )
14	13	eqeq2d	|- ( w = <. y , z >. -> ( x = [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X <-> x = X ) )
15	7 11 12 14	rexxpf	|- ( E. w e. ( B X. C ) x = [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X <-> E. y e. B E. z e. C x = X )
16	4 15	sylibr	|- ( ( ph /\ x e. A ) -> E. w e. ( B X. C ) x = [_ ( 1st ` w ) / y ]_ [_ ( 2nd ` w ) / z ]_ X )
17	1 5 16	wdom2d	|- ( ph -> A ~<_* ( B X. C ) )