Metamath Proof Explorer

Theorem unxpwdom3

Description: Weaker version of unxpwdom where a function is required only to be cancellative, not an injection. D and B are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into A , each row must hit an element of B ; by column injectivity, each row can be identified in at least one way by the B element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015)MOVABLE

Ref Expression
Hypotheses unxpwdom3.av 
|- ( ph -> A e. V )
unxpwdom3.bv 
|- ( ph -> B e. W )
unxpwdom3.dv 
|- ( ph -> D e. X )
unxpwdom3.ov 
|- ( ( ph /\ a e. C /\ b e. D ) -> ( a .+ b ) e. ( A u. B ) )
unxpwdom3.lc 
|- ( ( ( ph /\ a e. C ) /\ ( b e. D /\ c e. D ) ) -> ( ( a .+ b ) = ( a .+ c ) <-> b = c ) )
unxpwdom3.rc 
|- ( ( ( ph /\ d e. D ) /\ ( a e. C /\ c e. C ) ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )
unxpwdom3.ni 
|- ( ph -> -. D ~<_ A )
Assertion unxpwdom3 
|- ( ph -> C ~<_* ( D X. B ) )

Proof

Step Hyp Ref Expression
1 unxpwdom3.av 
 |-  ( ph -> A e. V )
2 unxpwdom3.bv 
 |-  ( ph -> B e. W )
3 unxpwdom3.dv 
 |-  ( ph -> D e. X )
4 unxpwdom3.ov 
 |-  ( ( ph /\ a e. C /\ b e. D ) -> ( a .+ b ) e. ( A u. B ) )
5 unxpwdom3.lc 
 |-  ( ( ( ph /\ a e. C ) /\ ( b e. D /\ c e. D ) ) -> ( ( a .+ b ) = ( a .+ c ) <-> b = c ) )
6 unxpwdom3.rc 
 |-  ( ( ( ph /\ d e. D ) /\ ( a e. C /\ c e. C ) ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )
7 unxpwdom3.ni 
 |-  ( ph -> -. D ~<_ A )
8 3 2 xpexd 
 |-  ( ph -> ( D X. B ) e. _V )
9 simprr 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) -> ( a .+ d ) e. B )
10 simplr 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) -> a e. C )
11 6 an4s 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ c e. C ) ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )
12 11 anassrs 
 |-  ( ( ( ( ph /\ a e. C ) /\ d e. D ) /\ c e. C ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )
13 12 adantlrr 
 |-  ( ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) /\ c e. C ) -> ( ( c .+ d ) = ( a .+ d ) <-> c = a ) )
14 10 13 riota5 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) -> ( iota_ c e. C ( c .+ d ) = ( a .+ d ) ) = a )
15 14 eqcomd 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) -> a = ( iota_ c e. C ( c .+ d ) = ( a .+ d ) ) )
16 eqeq2 
 |-  ( y = ( a .+ d ) -> ( ( c .+ d ) = y <-> ( c .+ d ) = ( a .+ d ) ) )
17 16 riotabidv 
 |-  ( y = ( a .+ d ) -> ( iota_ c e. C ( c .+ d ) = y ) = ( iota_ c e. C ( c .+ d ) = ( a .+ d ) ) )
18 17 rspceeqv 
 |-  ( ( ( a .+ d ) e. B /\ a = ( iota_ c e. C ( c .+ d ) = ( a .+ d ) ) ) -> E. y e. B a = ( iota_ c e. C ( c .+ d ) = y ) )
19 9 15 18 syl2anc 
 |-  ( ( ( ph /\ a e. C ) /\ ( d e. D /\ ( a .+ d ) e. B ) ) -> E. y e. B a = ( iota_ c e. C ( c .+ d ) = y ) )
20 7 adantr 
 |-  ( ( ph /\ a e. C ) -> -. D ~<_ A )
21 1 ad2antrr 
 |-  ( ( ( ph /\ a e. C ) /\ A. d e. D -. ( a .+ d ) e. B ) -> A e. V )
22 oveq2 
 |-  ( d = b -> ( a .+ d ) = ( a .+ b ) )
23 22 eleq1d 
 |-  ( d = b -> ( ( a .+ d ) e. B <-> ( a .+ b ) e. B ) )
24 23 notbid 
 |-  ( d = b -> ( -. ( a .+ d ) e. B <-> -. ( a .+ b ) e. B ) )
25 24 rspcv 
 |-  ( b e. D -> ( A. d e. D -. ( a .+ d ) e. B -> -. ( a .+ b ) e. B ) )
26 25 adantl 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( A. d e. D -. ( a .+ d ) e. B -> -. ( a .+ b ) e. B ) )
27 4 3expa 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( a .+ b ) e. ( A u. B ) )
28 elun 
 |-  ( ( a .+ b ) e. ( A u. B ) <-> ( ( a .+ b ) e. A \/ ( a .+ b ) e. B ) )
29 27 28 sylib 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( ( a .+ b ) e. A \/ ( a .+ b ) e. B ) )
30 29 orcomd 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( ( a .+ b ) e. B \/ ( a .+ b ) e. A ) )
31 30 ord 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( -. ( a .+ b ) e. B -> ( a .+ b ) e. A ) )
32 26 31 syld 
 |-  ( ( ( ph /\ a e. C ) /\ b e. D ) -> ( A. d e. D -. ( a .+ d ) e. B -> ( a .+ b ) e. A ) )
33 32 impancom 
 |-  ( ( ( ph /\ a e. C ) /\ A. d e. D -. ( a .+ d ) e. B ) -> ( b e. D -> ( a .+ b ) e. A ) )
34 5 ex 
 |-  ( ( ph /\ a e. C ) -> ( ( b e. D /\ c e. D ) -> ( ( a .+ b ) = ( a .+ c ) <-> b = c ) ) )
35 34 adantr 
 |-  ( ( ( ph /\ a e. C ) /\ A. d e. D -. ( a .+ d ) e. B ) -> ( ( b e. D /\ c e. D ) -> ( ( a .+ b ) = ( a .+ c ) <-> b = c ) ) )
36 33 35 dom2d 
 |-  ( ( ( ph /\ a e. C ) /\ A. d e. D -. ( a .+ d ) e. B ) -> ( A e. V -> D ~<_ A ) )
37 21 36 mpd 
 |-  ( ( ( ph /\ a e. C ) /\ A. d e. D -. ( a .+ d ) e. B ) -> D ~<_ A )
38 20 37 mtand 
 |-  ( ( ph /\ a e. C ) -> -. A. d e. D -. ( a .+ d ) e. B )
39 dfrex2 
 |-  ( E. d e. D ( a .+ d ) e. B <-> -. A. d e. D -. ( a .+ d ) e. B )
40 38 39 sylibr 
 |-  ( ( ph /\ a e. C ) -> E. d e. D ( a .+ d ) e. B )
41 19 40 reximddv 
 |-  ( ( ph /\ a e. C ) -> E. d e. D E. y e. B a = ( iota_ c e. C ( c .+ d ) = y ) )
42 vex 
 |-  d e. _V
43 vex 
 |-  y e. _V
44 42 43 op1std 
 |-  ( x = <. d , y >. -> ( 1st ` x ) = d )
45 44 oveq2d 
 |-  ( x = <. d , y >. -> ( c .+ ( 1st ` x ) ) = ( c .+ d ) )
46 42 43 op2ndd 
 |-  ( x = <. d , y >. -> ( 2nd ` x ) = y )
47 45 46 eqeq12d 
 |-  ( x = <. d , y >. -> ( ( c .+ ( 1st ` x ) ) = ( 2nd ` x ) <-> ( c .+ d ) = y ) )
48 47 riotabidv 
 |-  ( x = <. d , y >. -> ( iota_ c e. C ( c .+ ( 1st ` x ) ) = ( 2nd ` x ) ) = ( iota_ c e. C ( c .+ d ) = y ) )
49 48 eqeq2d 
 |-  ( x = <. d , y >. -> ( a = ( iota_ c e. C ( c .+ ( 1st ` x ) ) = ( 2nd ` x ) ) <-> a = ( iota_ c e. C ( c .+ d ) = y ) ) )
50 49 rexxp 
 |-  ( E. x e. ( D X. B ) a = ( iota_ c e. C ( c .+ ( 1st ` x ) ) = ( 2nd ` x ) ) <-> E. d e. D E. y e. B a = ( iota_ c e. C ( c .+ d ) = y ) )
51 41 50 sylibr 
 |-  ( ( ph /\ a e. C ) -> E. x e. ( D X. B ) a = ( iota_ c e. C ( c .+ ( 1st ` x ) ) = ( 2nd ` x ) ) )
52 8 51 wdomd 
 |-  ( ph -> C ~<_* ( D X. B ) )