# 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 ${⊢}{\phi }\to {A}\in {V}$
unxpwdom3.bv ${⊢}{\phi }\to {B}\in {W}$
unxpwdom3.dv ${⊢}{\phi }\to {D}\in {X}$
unxpwdom3.ov
unxpwdom3.lc
unxpwdom3.rc
unxpwdom3.ni ${⊢}{\phi }\to ¬{D}\preccurlyeq {A}$
Assertion unxpwdom3 ${⊢}{\phi }\to {C}{\preccurlyeq }^{*}\left({D}×{B}\right)$

### Proof

Step Hyp Ref Expression
1 unxpwdom3.av ${⊢}{\phi }\to {A}\in {V}$
2 unxpwdom3.bv ${⊢}{\phi }\to {B}\in {W}$
3 unxpwdom3.dv ${⊢}{\phi }\to {D}\in {X}$
4 unxpwdom3.ov
5 unxpwdom3.lc
6 unxpwdom3.rc
7 unxpwdom3.ni ${⊢}{\phi }\to ¬{D}\preccurlyeq {A}$
8 3 2 xpexd ${⊢}{\phi }\to {D}×{B}\in \mathrm{V}$
9 simprr
10 simplr
11 6 an4s
12 11 anassrs
14 10 13 riota5
15 14 eqcomd
16 eqeq2
17 16 riotabidv
18 17 rspceeqv
19 9 15 18 syl2anc
20 7 adantr ${⊢}\left({\phi }\wedge {a}\in {C}\right)\to ¬{D}\preccurlyeq {A}$
22 oveq2
23 22 eleq1d
24 23 notbid
25 24 rspcv
27 4 3expa
28 elun
29 27 28 sylib
30 29 orcomd
31 30 ord
32 26 31 syld
33 32 impancom
34 5 ex
36 33 35 dom2d
37 21 36 mpd
38 20 37 mtand
39 dfrex2
40 38 39 sylibr
41 19 40 reximddv
42 vex ${⊢}{d}\in \mathrm{V}$
43 vex ${⊢}{y}\in \mathrm{V}$
44 42 43 op1std ${⊢}{x}=⟨{d},{y}⟩\to {1}^{st}\left({x}\right)={d}$
45 44 oveq2d
46 42 43 op2ndd ${⊢}{x}=⟨{d},{y}⟩\to {2}^{nd}\left({x}\right)={y}$
47 45 46 eqeq12d
48 47 riotabidv
49 48 eqeq2d
50 49 rexxp
51 41 50 sylibr
52 8 51 wdomd ${⊢}{\phi }\to {C}{\preccurlyeq }^{*}\left({D}×{B}\right)$